use zero_extend_exprt in SMT2 front-end

kroening · kroening · commit b13bf9f6fd3b · 2024-11-04T08:13:31.000-08:00
This replaces the use of a typecast expression by zero_extend_exprt when
parsing an SMT-LIB2 zero_extend expression.
diff --git a/src/solvers/smt2/smt2_parser.cpp b/src/solvers/smt2/smt2_parser.cpp
@@ -693,9 +693,9 @@ exprt smt2_parsert::function_application()
           else if(id=="zero_extend")
           {
             auto width=to_unsignedbv_type(op[0].type()).get_width();
-            unsignedbv_typet unsigned_type(width+index);
+            unsignedbv_typet unsigned_type{width + index};
 
-            return typecast_exprt(op[0], unsigned_type);
+            return zero_extend_exprt{op[0], unsigned_type};
           }
           else if(id == ID_repeat)
           {

Original file line number	Diff line number	Diff line change
`@@ -693,9 +693,9 @@ exprt smt2_parsert::function_application()`
`693`	`693`	`else if(id=="zero_extend")`
`694`	`694`	`{`
`695`	`695`	`auto width=to_unsignedbv_type(op[0].type()).get_width();`
`696`		`- unsignedbv_typet unsigned_type(width+index);`
	`696`	`+ unsignedbv_typet unsigned_type{width + index};`
`697`	`697`
`698`		`- return typecast_exprt(op[0], unsigned_type);`
	`698`	`+ return zero_extend_exprt{op[0], unsigned_type};`
`699`	`699`	`}`
`700`	`700`	`else if(id == ID_repeat)`
`701`	`701`	`{`