From 1eb8803c1e437a9988b15b447c5baa0ba42e8cc2 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 24 Jan 2023 18:21:04 +0000 Subject: [PATCH] Array_UF21 does not always work with incremental SMT back-end 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. --- regression/cbmc/Array_UF21/test.desc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/regression/cbmc/Array_UF21/test.desc b/regression/cbmc/Array_UF21/test.desc index 8d4a044d982..e9d3c4ebe15 100644 --- 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$