Add regression tests for ---dump-smt-formula arg

Author: Enrico Steffinlongo

regression/cbmc-output-file/dump-smt-formula/cvc5-match-out-file-rules.txt

@@ -0,0 +1,9 @@
+\(set-option :produce-models true\)
+\(set-logic ALL\)
+\(define-fun B0 \(\) Bool true\)
+\(declare-fun |main::1::x!0@1#1| \(\) \(_ BitVec 32\)\)
+\(define-fun B1 \(\) Bool \(= |main::1::x!0@1#1| |main::1::x!0@1#1|\)\)
+\(assert \(not \(not \(= |main::1::x!0@1#1| \(_ bv0 32\)\)\)\)\)
+\(define-fun B2 \(\) Bool \(not false\)\)
+\(assert B2\)
+\(check-sat\)

regression/cbmc-output-file/dump-smt-formula/cvc5-match.desc

@@ -0,0 +1,11 @@
+CORE
+test.c
+--incremental-smt2-solver 'cvc5 --lang=smtlib2.6 --incremental' --slice-formula --dump-smt-formula %out-file-name%
+Passing problem to incremental SMT2 solving via "cvc5 --lang=smtlib2.6 --incremental"
+\[main.assertion.\d+\] line \d+ Nondeterministic int assert.: FAILURE
+Output file matches.
+^EXIT=0$
+^SIGNAL=0$
+--
+Test to check that the --dump-smt-formula argument is used correctly and that the output file
+matches the rules defined in test-outfile-rules.txt

regression/cbmc-output-file/dump-smt-formula/cvc5-no-match-out-file-rules.txt

@@ -0,0 +1,6 @@
+\(set-option :produce-models true\)
+\(set-logic ALL\)
+\(define-fun B0 \(\) Bool true\)
+\(define-fun B2 \(\) Bool \(not false\)\)
+\(check-sat\)
+\(assert B2\)

regression/cbmc-output-file/dump-smt-formula/cvc5-no-match.desc

@@ -0,0 +1,11 @@
+CORE
+test.c
+--incremental-smt2-solver 'cvc5 --lang=smtlib2.6 --incremental' --slice-formula --dump-smt-formula %out-file-name%
+Passing problem to incremental SMT2 solving via "cvc5 --lang=smtlib2.6 --incremental"
+\[main.assertion.\d+\] line \d+ Nondeterministic int assert.: FAILURE
+Output file does not match.
+^EXIT=1$
+^SIGNAL=0$
+--
+Test to check that the --dump-smt-formula argument is used correctly and that the output file does
+not match the rules defined in test-outfile-rules.txt

regression/cbmc-output-file/dump-smt-formula/test.c

@@ -0,0 +1,7 @@
+
+int main()
+{
+  int x;
+  __CPROVER_assert(x, "Nondeterministic int assert.");
+  return 0;
+}

regression/cbmc-output-file/dump-smt-formula/z3-match-out-file-rules.txt

@@ -0,0 +1,9 @@
+\(set-option :produce-models true\)
+\(set-logic ALL\)
+\(define-fun B0 \(\) Bool true\)
+\(declare-fun |main::1::x!0@1#1| \(\) \(_ BitVec 32\)\)
+\(define-fun B1 \(\) Bool \(= |main::1::x!0@1#1| |main::1::x!0@1#1|\)\)
+\(assert \(not \(not \(= |main::1::x!0@1#1| \(_ bv0 32\)\)\)\)\)
+\(define-fun B2 \(\) Bool \(not false\)\)
+\(assert B2\)
+\(check-sat\)

regression/cbmc-output-file/dump-smt-formula/z3-match.desc

@@ -0,0 +1,11 @@
+CORE
+test.c
+--incremental-smt2-solver 'z3 --smt2 -in' --slice-formula --dump-smt-formula %out-file-name%
+Passing problem to incremental SMT2 solving via "z3 --smt2 -in"
+\[main.assertion.\d+\] line \d+ Nondeterministic int assert.: FAILURE
+Output file matches.
+^EXIT=0$
+^SIGNAL=0$
+--
+Test to check that the --dump-smt-formula argument is used correctly and that the output file
+matches the rules defined in test-outfile-rules.txt

regression/cbmc-output-file/dump-smt-formula/z3-no-match-out-file-rules.txt

@@ -0,0 +1,6 @@
+\(set-option :produce-models true\)
+\(set-logic ALL\)
+\(define-fun B0 \(\) Bool true\)
+\(define-fun B2 \(\) Bool \(not false\)\)
+\(check-sat\)
+\(assert B2\)

regression/cbmc-output-file/dump-smt-formula/z3-no-match.desc

@@ -0,0 +1,11 @@
+CORE
+test.c
+--incremental-smt2-solver 'z3 --smt2 -in' --slice-formula --dump-smt-formula %out-file-name%
+Passing problem to incremental SMT2 solving via "z3 --smt2 -in"
+\[main.assertion.\d+\] line \d+ Nondeterministic int assert.: FAILURE
+Output file does not match.
+^EXIT=1$
+^SIGNAL=0$
+--
+Test to check that the --dump-smt-formula argument is used correctly and that the output file does
+not match the rules defined in test-outfile-rules.txt