SMT2 back-end: flatten with_exprt operands

.github/workflows/pull-request-checks.yaml

@@ -72,9 +72,10 @@ jobs:
           make TAGS="[!shouldfail]" -C jbmc/unit test IPASIR=$PWD/riss.git/riss
       - name: Run regression tests
         run: |
+          export PATH=$PATH:`pwd`/src/solvers
           make -C regression test-parallel JOBS=${{env.linux-vcpus}} LIBS="$PWD/riss.git/release/lib/libriss-coprocessor.a -lpthread" IPASIR=$PWD/riss.git/riss
           make -C regression/cbmc test-paths-lifo
-          env PATH=$PATH:`pwd`/src/solvers make -C regression/cbmc test-cprover-smt2
+          make -C regression/cbmc test-cprover-smt2
           make -C jbmc/regression test-parallel JOBS=${{env.linux-vcpus}}
       - name: Check cleanup
         run: |
@@ -153,9 +154,10 @@ jobs:
           make TAGS="[!shouldfail]" -C jbmc/unit test
       - name: Run regression tests
         run: |
+          export PATH=$PATH:`pwd`/src/solvers
           make -C regression test-parallel JOBS=${{env.linux-vcpus}}
           make -C regression/cbmc test-paths-lifo
-          env PATH=$PATH:`pwd`/src/solvers make -C regression/cbmc test-cprover-smt2
+          make -C regression/cbmc test-cprover-smt2
           make -C jbmc/regression test-parallel JOBS=${{env.linux-vcpus}}
 
   # This job has been copied from the one above it, and modified to only build CBMC
@@ -339,9 +341,10 @@ jobs:
           make TAGS="[!shouldfail]" -C jbmc/unit test
       - name: Run regression tests
         run: |
+          export PATH=$PATH:`pwd`/src/solvers
           make -C regression test-parallel JOBS=${{env.linux-vcpus}}
           make -C regression/cbmc test-paths-lifo
-          env PATH=$PATH:`pwd`/src/solvers make -C regression/cbmc test-cprover-smt2
+          make -C regression/cbmc test-cprover-smt2
           make -C jbmc/regression test-parallel JOBS=${{env.linux-vcpus}}
 
   # This job takes approximately 17 to 41 minutes
@@ -689,7 +692,9 @@ jobs:
       - name: Run JBMC unit tests
         run: cd jbmc/unit; ./unit_tests
       - name: Run regression tests
-        run: make -C regression test-parallel JOBS=4
+        run: |
+          export PATH=$PATH:`pwd`/src/solvers
+          make -C regression test-parallel JOBS=4
       - name: Run JBMC regression tests
         run: make -C jbmc/regression test-parallel JOBS=4
 
@@ -855,7 +860,9 @@ jobs:
       - name: Download minisat with make
         run: make -C src minisat2-download
       - name: Build CBMC with make
-        run: make CXX=clcache BUILD_ENV=MSVC -j${{env.windows-vcpus}} -C src
+        run: |
+          make CXX=clcache BUILD_ENV=MSVC -j${{env.windows-vcpus}} -C src
+          echo "$pwd\src\solvers;" >> $env:GITHUB_PATH
       - name: Build unit tests with make
         run: make CXX=clcache BUILD_ENV=MSVC -j${{env.windows-vcpus}} -C unit all
       - name: Build jbmc with make

regression/contracts-dfcc/CMakeLists.txt

@@ -41,10 +41,15 @@ add_test_pl_profile(
 #)
 
 # solver appears on the PATH in Windows already
-#if(NOT "${CMAKE_SYSTEM_NAME}" STREQUAL "Windows")
-#  set_property(
-#    TEST "cbmc-cprover-smt2-CORE"
-#    PROPERTY ENVIRONMENT
-#      "PATH=$ENV{PATH}:$<TARGET_FILE_DIR:smt2_solver>"
-#  )
-#endif()
+if(NOT "${CMAKE_SYSTEM_NAME}" STREQUAL "Windows")
+  set_property(
+    TEST "contracts-dfcc-CORE"
+    PROPERTY ENVIRONMENT
+      "PATH=$ENV{PATH}:$<TARGET_FILE_DIR:smt2_solver>"
+  )
+  set_property(
+    TEST "contracts-non-dfcc-CORE"
+    PROPERTY ENVIRONMENT
+      "PATH=$ENV{PATH}:$<TARGET_FILE_DIR:smt2_solver>"
+  )
+endif()

regression/contracts-dfcc/array_struct_smt/main.c

@@ -0,0 +1,17 @@
+typedef struct
+{
+  int coeffs[2];
+} mlk_poly;
+
+// clang-format off
+void mlk_poly_add(mlk_poly *r, const mlk_poly *b)
+  __CPROVER_ensures(r->coeffs[0] == __CPROVER_old(*r).coeffs[0] + b->coeffs[0])
+  __CPROVER_assigns(__CPROVER_object_upto(r, sizeof(mlk_poly)));
+// clang-format on
+
+int main()
+{
+  mlk_poly r[1];
+  mlk_poly b[1];
+  mlk_poly_add(&r[0], &b[0]);
+}

regression/contracts-dfcc/array_struct_smt/test.desc

@@ -0,0 +1,12 @@
+CORE
+main.c
+--dfcc main --replace-call-with-contract mlk_poly_add _ --no-array-field-sensitivity --cprover-smt2
+^\[mlk_poly_add.overflow.1\] line 8 arithmetic overflow on signed \+
+^\*\* 1 of \d+ failed
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+Make sure the SMT back-end produces valid SMT2 when structs and arrays are
+nested in each other.

src/solvers/smt2/smt2_conv.cpp

@@ -4400,50 +4400,63 @@ void smt2_convt::convert_with(const with_exprt &expr)
     }
     else
     {
+      auto convert_operand = [this](const exprt &op)
+      {
+        // may need to flatten array-theory arrays in there
+        if(op.type().id() == ID_array && use_array_theory(op))
+          flatten_array(op);
+        else if(op.type().id() == ID_bool)
+          flatten2bv(op);
+        else
+          convert_expr(op);
+      };
+
       std::size_t struct_width=boolbv_width(struct_type);
 
       // figure out the offset and width of the member
       const boolbv_widtht::membert &m =
         boolbv_width.get_member(struct_type, component_name);
 
-      out << "(let ((?withop ";
-      convert_expr(expr.old());
-      out << ")) ";
-
       if(m.width==struct_width)
       {
-        // the struct is the same as the member, no concat needed,
-        // ?withop won't be used
-        convert_expr(value);
-      }
-      else if(m.offset==0)
-      {
-        // the member is at the beginning
-        out << "(concat "
-            << "((_ extract " << (struct_width-1) << " "
-                              << m.width << ") ?withop) ";
-        convert_expr(value);
-        out << ")"; // concat
-      }
-      else if(m.offset+m.width==struct_width)
-      {
-        // the member is at the end
-        out << "(concat ";
-        convert_expr(value);
-        out << " ((_ extract " << (m.offset - 1) << " 0) ?withop))";
+        // the struct is the same as the member, no concat needed
+        convert_operand(value);
       }
       else
       {
-        // most general case, need two concat-s
-        out << "(concat (concat "
-            << "((_ extract " << (struct_width-1) << " "
-                              << (m.offset+m.width) << ") ?withop) ";
-        convert_expr(value);
-        out << ") ((_ extract " << (m.offset-1) << " 0) ?withop)";
-        out << ")"; // concat
-      }
+        out << "(let ((?withop ";
+        convert_operand(expr.old());
+        out << ")) ";
+
+        if(m.offset == 0)
+        {
+          // the member is at the beginning
+          out << "(concat "
+              << "((_ extract " << (struct_width - 1) << " " << m.width
+              << ") ?withop) ";
+          convert_operand(value);
+          out << ")"; // concat
+        }
+        else if(m.offset + m.width == struct_width)
+        {
+          // the member is at the end
+          out << "(concat ";
+          convert_operand(value);
+          out << " ((_ extract " << (m.offset - 1) << " 0) ?withop))";
+        }
+        else
+        {
+          // most general case, need two concat-s
+          out << "(concat (concat "
+              << "((_ extract " << (struct_width - 1) << " "
+              << (m.offset + m.width) << ") ?withop) ";
+          convert_operand(value);
+          out << ") ((_ extract " << (m.offset - 1) << " 0) ?withop)";
+          out << ")"; // concat
+        }
 
-      out << ")"; // let ?withop
+        out << ")"; // let ?withop
+      }
     }
   }
   else if(expr_type.id() == ID_union || expr_type.id() == ID_union_tag)