Merge pull request #7503 from tautschnig/bugfixes/7442-z3

tautschnig · web-flow · commit 26f400bf4f6d · 2023-01-30T18:24:40.000+01:00
SMT2 back-end: improve support for zero-sized components
diff --git a/regression/cbmc/Float-flags-no-simp1/test.desc b/regression/cbmc/Float-flags-no-simp1/test.desc
@@ -1,4 +1,4 @@
-CORE broken-smt-backend thorough-paths
+CORE broken-cprover-smt-backend thorough-paths
 main.c
 --floatbv --no-simplify
 ^EXIT=0$
diff --git a/regression/cbmc/Float-flags-simp1/test.desc b/regression/cbmc/Float-flags-simp1/test.desc
@@ -6,3 +6,7 @@ main.c
 ^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring
+--
+This test only fails when running with the SMT solver on MacOS (with an
+invariant failure: "floatbv expressions should be flattened when using FPA
+theory").
diff --git a/regression/cbmc/Float-no-simp3/test.desc b/regression/cbmc/Float-no-simp3/test.desc
@@ -1,4 +1,4 @@
-CORE broken-cprover-smt-backend
+CORE
 main.c
 --floatbv --no-simplify
 ^EXIT=0$
diff --git a/regression/cbmc/Float-no-simp9/test.desc b/regression/cbmc/Float-no-simp9/test.desc
@@ -1,4 +1,4 @@
-CORE broken-smt-backend thorough-paths
+CORE broken-cprover-smt-backend thorough-paths
 main.c
 --floatbv --no-simplify
 ^EXIT=0$
diff --git a/regression/cbmc/Multi_Dimensional_Array2/test.desc b/regression/cbmc/Multi_Dimensional_Array2/test.desc
@@ -1,4 +1,4 @@
-CORE broken-smt-backend new-smt-backend
+CORE broken-cprover-smt-backend new-smt-backend
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/Multi_Dimensional_Array3/test.desc b/regression/cbmc/Multi_Dimensional_Array3/test.desc
@@ -1,4 +1,4 @@
-CORE broken-smt-backend new-smt-backend
+CORE broken-cprover-smt-backend new-smt-backend
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/Pointer_byte_extract5/no-simplify.desc b/regression/cbmc/Pointer_byte_extract5/no-simplify.desc
@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE broken-cprover-smt-backend
 main.i
 --bounds-check --32 --no-simplify
 ^EXIT=10$
diff --git a/regression/cbmc/Quantifiers-assertion/test.desc b/regression/cbmc/Quantifiers-assertion/test.desc
@@ -1,4 +1,4 @@
-CORE broken-z3-smt-backend
+CORE
 main.c
 
 ^\*\* Results:$
diff --git a/regression/cbmc/Quantifiers-two-dimension-array/fixed.desc b/regression/cbmc/Quantifiers-two-dimension-array/fixed.desc
@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE broken-cprover-smt-backend
 fixed.c
 
 ^\*\* Results:$
diff --git a/regression/cbmc/byte_update12/test.desc b/regression/cbmc/byte_update12/test.desc
@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE broken-cprover-smt-backend
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/field-sensitivity16/test.desc b/regression/cbmc/field-sensitivity16/test.desc
@@ -1,4 +1,4 @@
-CORE broken-z3-smt-backend
+CORE
 main.c
 
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/cbmc/havoc_slice/test_struct_raw_bytes.desc b/regression/cbmc/havoc_slice/test_struct_raw_bytes.desc
@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE broken-cprover-smt-backend
 test_struct_raw_bytes.c
 
 ^EXIT=10$
diff --git a/regression/cbmc/integer-assignments1/test.desc b/regression/cbmc/integer-assignments1/test.desc
@@ -1,4 +1,4 @@
-CORE smt-backend broken-smt-backend
+CORE smt-backend broken-cprover-smt-backend
 main.c
 --trace --smt2
 ^EXIT=10$
diff --git a/regression/cbmc/memory_allocation1/test.desc b/regression/cbmc/memory_allocation1/test.desc
@@ -11,3 +11,5 @@ main.c
 ^VERIFICATION FAILED$
 --
 ^warning: ignoring
+--
+This test only fails when using SMT solvers as back-end on Windows.
diff --git a/regression/cbmc/printf1/test.desc b/regression/cbmc/printf1/test.desc
@@ -9,3 +9,6 @@ main.c
 ^PRINT f1 123\.000000, -123\.000000, 123\.123000, 0\.123000$
 --
 ^warning: ignoring
+--
+This test only fails when using SMT solvers as back-end on Windows ("TODO
+typecast3 floatbv -> pointer", same problem as va_list3).
diff --git a/regression/cbmc/union10/union_list2.desc b/regression/cbmc/union10/union_list2.desc
@@ -1,4 +1,4 @@
-CORE broken-z3-smt-backend
+CORE
 union_list2.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/union11/union_list.desc b/regression/cbmc/union11/union_list.desc
@@ -1,4 +1,4 @@
-CORE broken-z3-smt-backend
+CORE
 union_list.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/union12/test.desc b/regression/cbmc/union12/test.desc
@@ -13,3 +13,5 @@ Despite the large array inside the union, the test should complete within 10
 seconds. Simplify extractbits(concatenation(...)) is essential to make this
 possible. With 77236cc34 (Avoid nesting of ID_with/byte_update by rewriting
 byte_extract to use the root object) the test already is trivial, however.
+
+This test only fails when using SMT solvers as back-end on Windows.
diff --git a/regression/cbmc/va_list3/test.desc b/regression/cbmc/va_list3/test.desc
@@ -6,3 +6,6 @@ main.c
 ^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring
+--
+This test only fails when using SMT solvers as back-end on Windows ("TODO
+typecast3 floatbv -> pointer", same problem as va_list3).
diff --git a/regression/cbmc/void_pointer5/test.desc b/regression/cbmc/void_pointer5/test.desc
@@ -1,4 +1,4 @@
-CORE broken-smt-backend gcc-only
+CORE gcc-only
 main.c
 
 ^EXIT=10$
diff --git a/regression/cbmc/xml-trace/test.desc b/regression/cbmc/xml-trace/test.desc
@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE broken-cprover-smt-backend
 main.c
 --xml-ui --function test --little-endian
 activate-multi-line-match
diff --git a/regression/cbmc/z3/trace-char.desc b/regression/cbmc/z3/trace-char.desc
@@ -1,6 +1,6 @@
-CORE smt-backend broken-cprover-smt-backend
+CORE smt-backend
 trace-char.c
---trace --smt2 --z3
+--trace --z3
 ^EXIT=10$
 ^SIGNAL=0$
 arr=\{ '0', '1', '2', '3', '4', '5', '6', '7' \}
diff --git a/regression/cbmc/z3/trace.desc b/regression/cbmc/z3/trace.desc
@@ -1,6 +1,6 @@
-CORE smt-backend broken-cprover-smt-backend
+CORE smt-backend
 trace.c
---trace --smt2 --z3
+--trace --z3
 ^EXIT=10$
 ^SIGNAL=0$
 arr=\{ 0, 1, 2, 3, 4, 5, 6, 17 \}
diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp
diff --git a/src/solvers/smt2/smt2_conv.h b/src/solvers/smt2/smt2_conv.h

Original file line number	Diff line number	Diff line change
`@@ -1,4 +1,4 @@`
`1`		`-CORE broken-smt-backend thorough-paths`
	`1`	`+CORE broken-cprover-smt-backend thorough-paths`
`2`	`2`	`main.c`
`3`	`3`	`--floatbv --no-simplify`
`4`	`4`	`^EXIT=0$`
Original file line number	Diff line number	Diff line change
`@@ -1,4 +1,4 @@`
`1`		`-CORE broken-cprover-smt-backend`
	`1`	`+CORE`
`2`	`2`	`main.c`
`3`	`3`	`--floatbv --no-simplify`
`4`	`4`	`^EXIT=0$`
Original file line number	Diff line number	Diff line change
`@@ -1,4 +1,4 @@`
`1`		`-CORE broken-smt-backend new-smt-backend`
	`1`	`+CORE broken-cprover-smt-backend new-smt-backend`
`2`	`2`	`main.c`
`3`	`3`
`4`	`4`	`^EXIT=0$`
Original file line number	Diff line number	Diff line change
`@@ -1,4 +1,4 @@`
`1`		`-CORE broken-smt-backend`
	`1`	`+CORE broken-cprover-smt-backend`
`2`	`2`	`main.i`
`3`	`3`	`--bounds-check --32 --no-simplify`
`4`	`4`	`^EXIT=10$`
Original file line number	Diff line number	Diff line change
`@@ -1,4 +1,4 @@`
`1`		`-CORE broken-z3-smt-backend`
	`1`	`+CORE`
`2`	`2`	`main.c`
`3`	`3`
`4`	`4`	`^\\ Results:$`