Skip to content

Commit

Permalink
Fixed goto-synthesizer failing regression test
Browse files Browse the repository at this point in the history
  • Loading branch information
esteffin authored and Enrico Steffinlongo committed Dec 22, 2023
1 parent 7e527f9 commit 77705eb
Show file tree
Hide file tree
Showing 11 changed files with 11 additions and 11 deletions.
2 changes: 1 addition & 1 deletion regression/goto-synthesizer/array_uf/test.desc
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
CORE
main.c
--pointer-check _ --arrays-uf-always _ --arrays-uf-always
--pointer-check _ --no-malloc-may-fail --arrays-uf-always _ --arrays-uf-always
^EXIT=0$
^SIGNAL=0$
^VERIFICATION SUCCESSFUL$
Expand Down
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
CORE
main.c
--pointer-check
--pointer-check _ --no-malloc-may-fail _ --no-standard-checks
^EXIT=0$
^SIGNAL=0$
^\[main\.\d+\] line 10 Check loop invariant before entry: SUCCESS$
Expand Down
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
CORE
main.c
--pointer-check _ --dump-loop-contracts --json-output main.c
--pointer-check _ --no-malloc-may-fail --dump-loop-contracts --json-output main.c
^EXIT=0$
^SIGNAL=0$
\"sources"\: \[ \"main\.c\" \]
Expand Down
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
CORE
main.c
--pointer-check
--pointer-check _ --no-malloc-may-fail
^EXIT=0$
^SIGNAL=0$
^\[main.pointer\_dereference.\d+\] .* SUCCESS$
Expand Down
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
CORE
main.c
--pointer-check _ --dump-loop-contracts
--pointer-check _ --dump-loop-contracts --no-malloc-may-fail
^EXIT=0$
^SIGNAL=0$
\"sources"\: \[ \"main\.c\" \]
Expand Down
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
CORE
main.c
--pointer-check
--pointer-check _ --no-malloc-may-fail _ --no-standard-checks
^EXIT=0$
^SIGNAL=0$
^\[main.pointer\_dereference.\d+\] .* SUCCESS$
Expand Down
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
CORE
main.c
--pointer-check _ --sat-solver cadical --verbosity 10
--pointer-check _ --no-malloc-may-fail --sat-solver cadical --verbosity 10 _ --no-standard-checks
^EXIT=0$
^SIGNAL=0$
Solving with CaDiCaL|The specified solver, 'cadical', is not available. The default solver will be used instead.
Expand Down
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
CORE
main.c
--pointer-check _ --dump-loop-contracts
--pointer-check _ --no-malloc-may-fail --dump-loop-contracts
^EXIT=0$
^SIGNAL=0$
\"sources"\: \[ \"main\.c\" \]
Expand Down
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
CORE
main.c
--pointer-check _ --verbosity 9
--pointer-check _ --no-malloc-may-fail --verbosity 9
^EXIT=0$
^SIGNAL=0$
Quick filter\: 6.* out of 67 candidates were filtered out\.
Expand Down
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
CORE
main.c
--pointer-check _ --dump-loop-contracts
--pointer-check _ --no-malloc-may-fail --dump-loop-contracts
^EXIT=0$
^SIGNAL=0$
\"sources"\: \[ \"main\.c\" \]
Expand Down
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
CORE
main.c
--pointer-check
--pointer-check _ --no-malloc-may-fail _ --no-standard-checks
^EXIT=0$
^SIGNAL=0$
^\[main.pointer\_dereference.\d+\] .* SUCCESS$
Expand Down

0 comments on commit 77705eb

Please sign in to comment.