Merge pull request #3639 from diffblue/smt2-with-full-size

smt2: fix encoding of with expressions

Author: tautschnig

scripts/delete_failing_smt2_solver_tests

@@ -36,14 +36,12 @@ rm Float8/test.desc
 rm Linking4/test.desc
 rm Linking7/test.desc
 rm Linking7/member-name-mismatch.desc
-rm Malloc19/test.desc
 rm Malloc23/test.desc
 rm Malloc24/test.desc
 rm Memory_leak2/test.desc
 rm Multi_Dimensional_Array2/test.desc
 rm Overflow_Leftshift1/test.desc
 rm Overflow_Subtraction1/test.desc
-rm Pointer_Arithmetic10/test.desc
 rm Pointer_Arithmetic11/test.desc
 rm Pointer_byte_extract2/test.desc
 rm Pointer_byte_extract3/test.desc
@@ -87,7 +85,6 @@ rm pointer-function-parameters-struct-simple-recursion-2/test.desc
 rm pointer-function-parameters-struct-simple-recursion-3/test.desc
 rm scanf1/test.desc
 rm stack-trace/test.desc
-rm struct10/test.desc
 rm struct6/test.desc
 rm struct7/test.desc
 rm struct9/test.desc

src/solvers/smt2/smt2_conv.cpp

@@ -3476,7 +3476,7 @@ void smt2_convt::convert_with(const with_exprt &expr)
   {
     std::size_t s=expr.operands().size();
 
-    // strip of the trailing two operands
+    // strip off the trailing two operands
     with_exprt tmp = expr;
     tmp.operands().resize(s-2);
 
@@ -3515,7 +3515,7 @@ void smt2_convt::convert_with(const with_exprt &expr)
       std::size_t sub_width=boolbv_width(array_type.subtype());
       std::size_t index_width=boolbv_width(expr.where().type());
 
-      // We mask out the updated bit with AND,
+      // We mask out the updated bits with AND,
       // and then OR-in the shifted new value.
 
       out << "(let ((distance? ";
@@ -3540,15 +3540,16 @@ void smt2_convt::convert_with(const with_exprt &expr)
 
       out << "(bvor ";
       out << "(bvand ";
-      out << "(bvlshr (_ bv" << power(2, array_width)-1 << " "
-          << array_width << ") ";
-      out << "distance?) ";
+      out << "(bvnot ";
+      out << "(bvshl (_ bv" << power(2, sub_width) - 1 << " " << array_width
+          << ") ";
+      out << "distance?)) "; // bvnot, bvlshl
       convert_expr(expr.old());
       out << ") "; // bvand
-      out << "(bvlshr ";
+      out << "(bvshl ";
       out << "((_ zero_extend " << array_width-sub_width << ") ";
       convert_expr(expr.new_value());
-      out << ") distance?)))"; // zero_extend, bvlshr, bvor, let
+      out << ") distance?)))"; // zero_extend, bvshl, bvor, let
     }
   }
   else if(expr_type.id()==ID_struct)
@@ -3588,8 +3589,9 @@ void smt2_convt::convert_with(const with_exprt &expr)
 
       if(m.width==struct_width)
       {
-        // the struct is the same as the member, no concat needed
-        out << "?withop";
+        // the struct is the same as the member, no concat needed,
+        // ?withop won't be used
+        convert_expr(value);
       }
       else if(m.offset==0)
       {