diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2021-06-02 10:01:07 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-06-02 10:01:07 -0700 |
| commit | adb0ca274a1294e251fa5bca030ad54406fe26df (patch) | |
| tree | ae4df4998a18e1d22b7cd371b243b809a4eaffdf /test/regress/regress0 | |
| parent | 5f827e53d2dcd80a3cc679454de0b40108f01d93 (diff) | |
| parent | 338982182dbdabecf6f3b06e659621cf43bed916 (diff) | |
Merge branch 'master' into issue6661
Diffstat (limited to 'test/regress/regress0')
5 files changed, 60 insertions, 0 deletions
diff --git a/test/regress/regress0/bv/core/bitvec1.smtv1.smt2 b/test/regress/regress0/bv/core/bitvec1.smtv1.smt2 index 58cde43c2..78dd44d66 100644 --- a/test/regress/regress0/bv/core/bitvec1.smtv1.smt2 +++ b/test/regress/regress0/bv/core/bitvec1.smtv1.smt2 @@ -1,3 +1,5 @@ +; COMMAND-LINE: --no-check-proofs +; EXPECT: unsat (set-option :incremental false) (set-info :source "Hand-crafted bit-vector benchmarks. Some are from the SVC benchmark suite. Contributed by Vijay Ganesh (vganesh@stanford.edu). Translated into SMT-LIB diff --git a/test/regress/regress0/bv/core/bitvec3.smtv1.smt2 b/test/regress/regress0/bv/core/bitvec3.smtv1.smt2 index bb8c0f7e0..b149c0570 100644 --- a/test/regress/regress0/bv/core/bitvec3.smtv1.smt2 +++ b/test/regress/regress0/bv/core/bitvec3.smtv1.smt2 @@ -1,3 +1,5 @@ +; COMMAND-LINE: --no-check-proofs +; EXPECT: unsat (set-option :incremental false) (set-info :source "Hand-crafted bit-vector benchmarks. Some are from the SVC benchmark suite. Contributed by Vijay Ganesh (vganesh@stanford.edu). Translated into SMT-LIB diff --git a/test/regress/regress0/bv/core/constant_core.smt2 b/test/regress/regress0/bv/core/constant_core.smt2 index a353a5c6f..f9d2e022d 100644 --- a/test/regress/regress0/bv/core/constant_core.smt2 +++ b/test/regress/regress0/bv/core/constant_core.smt2 @@ -1,3 +1,5 @@ +; COMMAND-LINE: --no-check-proofs +; EXPECT: unsat (set-logic QF_BV) (set-info :smt-lib-version 2.6) (set-info :category "crafted") diff --git a/test/regress/regress0/proofs/issue277-circuit-propagator.smt2 b/test/regress/regress0/proofs/issue277-circuit-propagator.smt2 new file mode 100644 index 000000000..f0815e8f2 --- /dev/null +++ b/test/regress/regress0/proofs/issue277-circuit-propagator.smt2 @@ -0,0 +1,47 @@ +; EXPECT: sat +; EXPECT: sat +; EXPECT: sat +; EXPECT: sat +; EXPECT: sat +; EXPECT: sat +(set-logic QF_UF) +(set-option :produce-proofs true) +(set-option :incremental true) +(declare-fun p () Bool) +(declare-fun q () Bool) + +(push) +(assert (not (= p (not q)))) +(assert p) +(check-sat) +(pop) + +(push) +(assert (not (= (not q) p))) +(assert p) +(check-sat) +(pop) + +(push) +(assert (not (= (not p) (not (not q))))) +(assert p) +(check-sat) +(pop) + +(push) +(assert (not (= (not (not q)) (not p)))) +(assert p) +(check-sat) +(pop) + +(push) +(assert (not (= (not (not p)) (not (not (not q)))))) +(assert p) +(check-sat) +(pop) + +(push) +(assert (not (= (not (not (not q))) (not (not p))))) +(assert p) +(check-sat) +(pop)
\ No newline at end of file diff --git a/test/regress/regress0/strings/issue6643-ctn-decompose-conflict.smt2 b/test/regress/regress0/strings/issue6643-ctn-decompose-conflict.smt2 new file mode 100644 index 000000000..41a515640 --- /dev/null +++ b/test/regress/regress0/strings/issue6643-ctn-decompose-conflict.smt2 @@ -0,0 +1,7 @@ +; COMMAND-LINE: --strings-exp +(set-logic QF_SLIA) +(declare-fun y () String) +(declare-fun z () String) +(assert (not (= (str.contains y (str.replace "A" "" z)) (str.contains y "A")))) +(set-info :status sat) +(check-sat) |