smt-lib backend: generate annotated_pointer_constant_exprt

kroening · kroening · commit 39c3460cf1d3 · 2022-04-27T22:14:30.000+01:00
This mirrors the output of the flattening solver.
diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp
@@ -662,7 +662,9 @@ exprt smt2_convt::parse_rec(const irept &src, const typet &type)
     pointer_logict::pointert ptr;
     ptr.object = numeric_cast_v<std::size_t>(v / pow);
     ptr.offset=v%pow;
-    return pointer_logic.pointer_expr(ptr, to_pointer_type(type));
+    return annotated_pointer_constant_exprt(
+      bv_expr.get_value(),
+      pointer_logic.pointer_expr(ptr, to_pointer_type(type)));
   }
   else if(type.id()==ID_struct)
   {

Original file line number	Diff line number	Diff line change
`@@ -662,7 +662,9 @@ exprt smt2_convt::parse_rec(const irept &src, const typet &type)`
`662`	`662`	`pointer_logict::pointert ptr;`
`663`	`663`	`ptr.object = numeric_cast_v<std::size_t>(v / pow);`
`664`	`664`	`ptr.offset=v%pow;`
`665`		`- return pointer_logic.pointer_expr(ptr, to_pointer_type(type));`
	`665`	`+ return annotated_pointer_constant_exprt(`
	`666`	`+ bv_expr.get_value(),`
	`667`	`+ pointer_logic.pointer_expr(ptr, to_pointer_type(type)));`
`666`	`668`	`}`
`667`	`669`	`else if(type.id()==ID_struct)`
`668`	`670`	`{`