Merge pull request #8084 from esteffin/esteffin/other-smt2-reg-test-passing

thomasspriggs · web-flow · commit c0fe5a8a45af · 2023-11-28T15:27:31.000Z
Run additional regressions with new SMT solver
diff --git a/regression/cbmc/dynamic_size1/stack_object.desc b/regression/cbmc/dynamic_size1/stack_object.desc
@@ -1,4 +1,4 @@
-CORE no-new-smt
+CORE
 stack_object.c
 --pointer-check
 ^EXIT=0$
diff --git a/regression/cbmc/ptr_arithmetic_on_null/type_conflict.desc b/regression/cbmc/ptr_arithmetic_on_null/type_conflict.desc
@@ -1,4 +1,4 @@
-CORE gcc-only no-new-smt
+CORE gcc-only
 main.c
 -DMISSING_CAST
 pointer subtraction over different types

Original file line number	Diff line number	Diff line change
`@@ -1,4 +1,4 @@`
`1`		`-CORE gcc-only no-new-smt`
	`1`	`+CORE gcc-only`
`2`	`2`	`main.c`
`3`	`3`	`-DMISSING_CAST`
`4`	`4`	`pointer subtraction over different types`