File tree Expand file tree Collapse file tree 9 files changed +81
-0
lines changed
regression/cbmc-output-file/dump-smt-formula Expand file tree Collapse file tree 9 files changed +81
-0
lines changed Original file line number Diff line number Diff line change
1
+ \(set-option :produce-models true\)
2
+ \(set-logic ALL\)
3
+ \(define-fun B0 \(\) Bool true\)
4
+ \(declare-fun |main::1::x!0@1#1| \(\) \(_ BitVec 32\)\)
5
+ \(define-fun B1 \(\) Bool \(= |main::1::x!0@1#1| |main::1::x!0@1#1|\)\)
6
+ \(assert \(not \(not \(= |main::1::x!0@1#1| \(_ bv0 32\)\)\)\)\)
7
+ \(define-fun B2 \(\) Bool \(not false\)\)
8
+ \(assert B2\)
9
+ \(check-sat\)
Original file line number Diff line number Diff line change
1
+ CORE
2
+ test.c
3
+ --incremental-smt2-solver 'cvc5 --lang=smtlib2.6 --incremental' --slice-formula --dump-smt-formula %out-file-name%
4
+ Passing problem to incremental SMT2 solving via "cvc5 --lang=smtlib2.6 --incremental"
5
+ \[main.assertion.\d+\] line \d+ Nondeterministic int assert.: FAILURE
6
+ Output file matches.
7
+ ^EXIT=0$
8
+ ^SIGNAL=0$
9
+ --
10
+ Test to check that the --dump-smt-formula argument is used correctly and that the output file
11
+ matches the rules defined in test-outfile-rules.txt
Original file line number Diff line number Diff line change
1
+ \(set-option :produce-models true\)
2
+ \(set-logic ALL\)
3
+ \(define-fun B0 \(\) Bool true\)
4
+ \(define-fun B2 \(\) Bool \(not false\)\)
5
+ \(check-sat\)
6
+ \(assert B2\)
Original file line number Diff line number Diff line change
1
+ CORE
2
+ test.c
3
+ --incremental-smt2-solver 'cvc5 --lang=smtlib2.6 --incremental' --slice-formula --dump-smt-formula %out-file-name%
4
+ Passing problem to incremental SMT2 solving via "cvc5 --lang=smtlib2.6 --incremental"
5
+ \[main.assertion.\d+\] line \d+ Nondeterministic int assert.: FAILURE
6
+ Output file does not match.
7
+ ^EXIT=1$
8
+ ^SIGNAL=0$
9
+ --
10
+ Test to check that the --dump-smt-formula argument is used correctly and that the output file does
11
+ not match the rules defined in test-outfile-rules.txt
Original file line number Diff line number Diff line change
1
+
2
+ int main ()
3
+ {
4
+ int x ;
5
+ __CPROVER_assert (x , "Nondeterministic int assert." );
6
+ return 0 ;
7
+ }
Original file line number Diff line number Diff line change
1
+ \(set-option :produce-models true\)
2
+ \(set-logic ALL\)
3
+ \(define-fun B0 \(\) Bool true\)
4
+ \(declare-fun |main::1::x!0@1#1| \(\) \(_ BitVec 32\)\)
5
+ \(define-fun B1 \(\) Bool \(= |main::1::x!0@1#1| |main::1::x!0@1#1|\)\)
6
+ \(assert \(not \(not \(= |main::1::x!0@1#1| \(_ bv0 32\)\)\)\)\)
7
+ \(define-fun B2 \(\) Bool \(not false\)\)
8
+ \(assert B2\)
9
+ \(check-sat\)
Original file line number Diff line number Diff line change
1
+ CORE
2
+ test.c
3
+ --incremental-smt2-solver 'z3 --smt2 -in' --slice-formula --dump-smt-formula %out-file-name%
4
+ Passing problem to incremental SMT2 solving via "z3 --smt2 -in"
5
+ \[main.assertion.\d+\] line \d+ Nondeterministic int assert.: FAILURE
6
+ Output file matches.
7
+ ^EXIT=0$
8
+ ^SIGNAL=0$
9
+ --
10
+ Test to check that the --dump-smt-formula argument is used correctly and that the output file
11
+ matches the rules defined in test-outfile-rules.txt
Original file line number Diff line number Diff line change
1
+ \(set-option :produce-models true\)
2
+ \(set-logic ALL\)
3
+ \(define-fun B0 \(\) Bool true\)
4
+ \(define-fun B2 \(\) Bool \(not false\)\)
5
+ \(check-sat\)
6
+ \(assert B2\)
Original file line number Diff line number Diff line change
1
+ CORE
2
+ test.c
3
+ --incremental-smt2-solver 'z3 --smt2 -in' --slice-formula --dump-smt-formula %out-file-name%
4
+ Passing problem to incremental SMT2 solving via "z3 --smt2 -in"
5
+ \[main.assertion.\d+\] line \d+ Nondeterministic int assert.: FAILURE
6
+ Output file does not match.
7
+ ^EXIT=1$
8
+ ^SIGNAL=0$
9
+ --
10
+ Test to check that the --dump-smt-formula argument is used correctly and that the output file does
11
+ not match the rules defined in test-outfile-rules.txt
You can’t perform that action at this time.
0 commit comments