Array_UF21 does not always work with incremental SMT back-end

tautschnig · tautschnig · commit 1eb8803c1e43 · 2023-01-24T18:21:04.000Z
The test consistently fails when doing coverage checking (was also the case in the coverage check run of #7434, which was the PR introducing this test). The output is: `Invalid SMT response "corrupted"` The test appears to be working fine when not doing coverage checking, though.
diff --git a/regression/cbmc/Array_UF21/test.desc b/regression/cbmc/Array_UF21/test.desc
@@ -1,4 +1,4 @@
-CORE new-smt-backend
+CORE
 main.c
 --arrays-uf-always --bounds-check
 ^VERIFICATION FAILED$

Original file line number	Diff line number	Diff line change
`@@ -1,4 +1,4 @@`
`1`		`-CORE new-smt-backend`
	`1`	`+CORE`
`2`	`2`	`main.c`
`3`	`3`	`--arrays-uf-always --bounds-check`
`4`	`4`	`^VERIFICATION FAILED$`