diff options
Diffstat (limited to 'test/regress/regress0')
30 files changed, 209 insertions, 26 deletions
diff --git a/test/regress/regress0/arith/issue3480.smt2 b/test/regress/regress0/arith/issue3480.smt2 index 7609ad3e7..74ce8d32b 100644 --- a/test/regress/regress0/arith/issue3480.smt2 +++ b/test/regress/regress0/arith/issue3480.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --quiet +; COMMAND-LINE: --theoryof-mode=type --quiet (set-logic QF_NIA) (declare-fun a () Int) (declare-fun b () Int) diff --git a/test/regress/regress0/arith/issue4367.smt2 b/test/regress/regress0/arith/issue4367.smt2 new file mode 100644 index 000000000..abe5b09fd --- /dev/null +++ b/test/regress/regress0/arith/issue4367.smt2 @@ -0,0 +1,11 @@ +; COMMAND-LINE: --incremental --check-unsat-cores +; EXPECT: unsat +; EXPECT: unsat +(set-logic NRA) +(declare-const r0 Real) +(assert (! (forall ((q0 Bool) (q1 Real)) (= (* r0 r0) r0 r0)) :named IP_2)) +(assert (! (not (forall ((q2 Real)) (not (<= 55.033442 r0 55.033442 q2)))) :named IP_5)) +(push 1) +(check-sat) +(pop 1) +(check-sat) diff --git a/test/regress/regress0/arith/issue4525.smt2 b/test/regress/regress0/arith/issue4525.smt2 new file mode 100644 index 000000000..ae7e00990 --- /dev/null +++ b/test/regress/regress0/arith/issue4525.smt2 @@ -0,0 +1,4 @@ +(set-logic QF_NRAT) +(assert (> (cot 0.0) (/ 1 0))) +(set-info :status unsat) +(check-sat) diff --git a/test/regress/regress0/bv/bv_to_int_elim_err.smt2 b/test/regress/regress0/bv/bv_to_int_elim_err.smt2 new file mode 100644 index 000000000..16731b01e --- /dev/null +++ b/test/regress/regress0/bv/bv_to_int_elim_err.smt2 @@ -0,0 +1,7 @@ +; COMMAND-LINE: --solve-bv-as-int=1 --no-check-models +; EXPECT: sat +(set-logic QF_BV) +(declare-fun _substvar_183_ () (_ BitVec 32)) +(assert (let ((?x15 ((_ sign_extend 0) _substvar_183_))) (bvsle ((_ zero_extend 24) ((_ extract 15 8) (bvadd ?x15 (_ bv4294966758 32)))) (bvadd ?x15 ?x15)))) +(check-sat) +(exit) diff --git a/test/regress/regress0/bv/issue-4075.smt2 b/test/regress/regress0/bv/issue-4075.smt2 new file mode 100644 index 000000000..083fbf897 --- /dev/null +++ b/test/regress/regress0/bv/issue-4075.smt2 @@ -0,0 +1,11 @@ +; REQUIRES: no-competition +; EXPECT: (error "Parse Error: issue-4075.smt2:11.26: expecting number of repeats > 0 +; EXPECT: +; EXPECT: (simplify ((_ repeat 0) b)) +; EXPECT: ^ +; EXPECT:") +; EXIT: 1 +(set-logic QF_BV) +(define-sort a () (_ BitVec 4)) +(declare-const b a) +(simplify ((_ repeat 0) b)) diff --git a/test/regress/regress0/bv/issue-4076.smt2 b/test/regress/regress0/bv/issue-4076.smt2 new file mode 100644 index 000000000..c52d2169a --- /dev/null +++ b/test/regress/regress0/bv/issue-4076.smt2 @@ -0,0 +1,14 @@ +; COMMAND-LINE: --incremental +; EXPECT: sat +; EXPECT: sat +(set-logic ALL) +(declare-fun a ((_ BitVec 2)) Int) +(declare-fun b (Int) (_ BitVec 2)) +(declare-const c Int) +(declare-const d Int) +(assert (= (a #b01) 1)) +(assert(= 0 (a (bvlshr (b c) (b d))))) +(push) +(check-sat) +(pop) +(check-sat) diff --git a/test/regress/regress0/bv/issue-4130.smt2 b/test/regress/regress0/bv/issue-4130.smt2 new file mode 100644 index 000000000..4c7daab57 --- /dev/null +++ b/test/regress/regress0/bv/issue-4130.smt2 @@ -0,0 +1,11 @@ +; REQUIRES: no-competition +; EXPECT: (error "Parse Error: issue-4130.smt2:10.39: expecting bit-width > 0 +; EXPECT: +; EXPECT: (assert (and (= a (bv2nat ((_ int2bv 0) a))))) +; EXPECT: ^ +; EXPECT: ") +; EXIT: 1 +(set-logic ALL) +(declare-fun a () Int) +(assert (and (= a (bv2nat ((_ int2bv 0) a))))) +(check-sat) diff --git a/test/regress/regress0/eqrange1.smt2 b/test/regress/regress0/eqrange1.smt2 new file mode 100644 index 000000000..90eb7a22a --- /dev/null +++ b/test/regress/regress0/eqrange1.smt2 @@ -0,0 +1,15 @@ +(set-logic QF_AUFBV) +(set-option :arrays-exp true) +(set-option :quiet true) ; Suppress check-model warnings involving quantifiers +(set-info :status sat) +(declare-fun a1 () (Array (_ BitVec 2) (_ BitVec 2))) +(declare-fun a2 () (Array (_ BitVec 2) (_ BitVec 2))) +(declare-fun e1 () (_ BitVec 2)) +(declare-fun e2 () (_ BitVec 2)) +(assert (distinct e1 e2)) +(assert (= a1 (store (store (store (store a1 #b00 e1) #b01 e1) #b10 e1) #b11 e1))) +(assert (= a2 (store (store (store (store a2 #b00 e1) #b01 e1) #b10 e2) #b11 e1))) +(assert (eqrange a1 a2 #b00 #b01)) +(assert (eqrange a1 a2 #b11 #b11)) +(check-sat) +(exit) diff --git a/test/regress/regress0/eqrange2.smt2 b/test/regress/regress0/eqrange2.smt2 new file mode 100644 index 000000000..efddbc88b --- /dev/null +++ b/test/regress/regress0/eqrange2.smt2 @@ -0,0 +1,12 @@ +(set-logic AUFBV) +(set-option :arrays-exp true) +(set-info :status unsat) +(declare-sort Element 0) +(declare-const a (Array (_ BitVec 3) Element)) +(declare-const b (Array (_ BitVec 3) Element)) +(declare-const j (_ BitVec 3)) +(assert (eqrange a b (_ bv0 3) j)) +(assert (eqrange a b (bvadd j (_ bv1 3)) (_ bv7 3))) +(assert (exists ((i (_ BitVec 3))) (not (= (select a i) (select b i))))) +(check-sat) +(exit) diff --git a/test/regress/regress0/eqrange3.smt2 b/test/regress/regress0/eqrange3.smt2 new file mode 100644 index 000000000..54e9d0386 --- /dev/null +++ b/test/regress/regress0/eqrange3.smt2 @@ -0,0 +1,16 @@ +(set-logic QF_AUFLIA) +(set-option :arrays-exp true) +(set-option :quiet true) ; Suppress Warning +(set-info :status sat) +(declare-fun a1 () (Array Int Int)) +(declare-fun a2 () (Array Int Int)) +(declare-fun e1 () Int) +(declare-fun e2 () Int) +(assert (distinct e1 e2)) +(assert (= a1 (store (store (store (store a1 0 e1) 1 e1) 2 e1) 3 e1))) +(assert (= a2 (store (store (store (store a2 1 e1) 0 e1) 2 e2) 3 e1))) +(assert (eqrange a1 a2 (- 1) 1)) +(assert (eqrange a1 a2 3 3)) +(check-sat) +(exit) + diff --git a/test/regress/regress0/fp/ext-rew-test.smt2 b/test/regress/regress0/fp/ext-rew-test.smt2 index 3fb3a9e53..726487e18 100644 --- a/test/regress/regress0/fp/ext-rew-test.smt2 +++ b/test/regress/regress0/fp/ext-rew-test.smt2 @@ -1,3 +1,4 @@ +; REQUIRES: symfpu ; COMMAND-LINE: --ext-rew-prep --ext-rew-prep-agg ; EXPECT: unsat (set-info :smt-lib-version 2.6) diff --git a/test/regress/regress0/ho/issue4477.smt2 b/test/regress/regress0/ho/issue4477.smt2 new file mode 100644 index 000000000..7162d260c --- /dev/null +++ b/test/regress/regress0/ho/issue4477.smt2 @@ -0,0 +1,11 @@ +; REQUIRES: no-competition +; SCRUBBER: grep -o "Symbol '->' not declared" +; EXPECT: Symbol '->' not declared +; EXIT: 1 +(set-logic ALL) +(declare-sort s 0) +(declare-fun a () s) +(declare-fun b () s) +(declare-fun c (s) s) +(assert (forall ((d (-> s s))) (distinct (d a) (c a) b))) +(check-sat) diff --git a/test/regress/regress0/nl/issue3729-cm-solved-tf.smt2 b/test/regress/regress0/nl/issue3729-cm-solved-tf.smt2 index 69bb74e84..75d4b6e3a 100644 --- a/test/regress/regress0/nl/issue3729-cm-solved-tf.smt2 +++ b/test/regress/regress0/nl/issue3729-cm-solved-tf.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --quiet +; COMMAND-LINE: --quiet --no-check-models ; EXPECT: sat (set-logic QF_NRAT) (set-info :status sat) diff --git a/test/regress/regress0/printer/bv_consts_bin.smt2 b/test/regress/regress0/printer/bv_consts_bin.smt2 index e5c3c2824..f910c2c96 100644 --- a/test/regress/regress0/printer/bv_consts_bin.smt2 +++ b/test/regress/regress0/printer/bv_consts_bin.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --bv-print-consts-in-binary +; COMMAND-LINE: ; EXPECT: sat ; EXPECT: ((x #b0001)) (set-option :produce-models true) diff --git a/test/regress/regress0/printer/bv_consts_dec.smt2 b/test/regress/regress0/printer/bv_consts_dec.smt2 index 98d95e822..38337e8cf 100644 --- a/test/regress/regress0/printer/bv_consts_dec.smt2 +++ b/test/regress/regress0/printer/bv_consts_dec.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --no-bv-print-consts-in-binary +; COMMAND-LINE: --bv-print-consts-as-indexed-symbols ; EXPECT: sat ; EXPECT: ((x (_ bv1 4))) (set-option :produce-models true) diff --git a/test/regress/regress0/printer/empty_symbol_name.smt2 b/test/regress/regress0/printer/empty_symbol_name.smt2 index 46652bc24..41d1ffd84 100644 --- a/test/regress/regress0/printer/empty_symbol_name.smt2 +++ b/test/regress/regress0/printer/empty_symbol_name.smt2 @@ -1,5 +1,5 @@ ; EXPECT: sat -; EXPECT: ((|| (_ bv1 4))) +; EXPECT: ((|| #b0001)) (set-option :produce-models true) (set-logic QF_BV) (declare-const || (_ BitVec 4)) diff --git a/test/regress/regress0/printer/symbol_starting_w_digit.smt2 b/test/regress/regress0/printer/symbol_starting_w_digit.smt2 index 6a688a16f..ea13a65c2 100644 --- a/test/regress/regress0/printer/symbol_starting_w_digit.smt2 +++ b/test/regress/regress0/printer/symbol_starting_w_digit.smt2 @@ -1,6 +1,6 @@ ; EXPECT: sat -; EXPECT: ((|0_0| (_ bv1 4))) -; EXPECT: ((x (_ bv3 4))) +; EXPECT: ((|0_0| #b0001)) +; EXPECT: ((x #b0011)) (set-option :produce-models true) (set-logic QF_BV) (declare-const |0_0| (_ BitVec 4)) diff --git a/test/regress/regress0/quantifiers/issue4437-unc-quant.smt2 b/test/regress/regress0/quantifiers/issue4437-unc-quant.smt2 new file mode 100644 index 000000000..5dd51dc0c --- /dev/null +++ b/test/regress/regress0/quantifiers/issue4437-unc-quant.smt2 @@ -0,0 +1,9 @@ +; REQUIRES: no-competition +; EXPECT: Quantifier used in non-quantified logic +; SCRUBBER: grep -o "Quantifier used in non-quantified logic" +; EXIT: 1 +(set-logic QF_AUFBVLIA) +(declare-fun a () (_ BitVec 8)) +(declare-fun b () (_ BitVec 8)) +(assert (forall ((c (_ BitVec 8))) (= (bvashr c a) b))) +(check-sat) diff --git a/test/regress/regress0/quantifiers/issue4476-ext-rew.smt2 b/test/regress/regress0/quantifiers/issue4476-ext-rew.smt2 new file mode 100644 index 000000000..c54254e67 --- /dev/null +++ b/test/regress/regress0/quantifiers/issue4476-ext-rew.smt2 @@ -0,0 +1,5 @@ +(set-logic NRA) +(set-info :status sat) +(set-option :ext-rewrite-quant true) +(assert (exists ((a Real) (b Real)) (forall ((c Real)) (= (/ b (/ 1 c)) 0)))) +(check-sat) diff --git a/test/regress/regress0/quantifiers/issue4576.smt2 b/test/regress/regress0/quantifiers/issue4576.smt2 new file mode 100644 index 000000000..3cb99b84a --- /dev/null +++ b/test/regress/regress0/quantifiers/issue4576.smt2 @@ -0,0 +1,5 @@ +; EXPECT: unsat +(set-logic NRA) +(declare-const r0 Real) +(assert (exists ((q36 Real) (q37 Bool) (q38 Bool) (q39 Bool) (q40 Real) (q41 Bool)) (= 0.0 0.0 (/ 437686.0 r0) 0.0 0.96101))) +(check-sat) diff --git a/test/regress/regress0/smtlib/define-fun-rec-logic.smt2 b/test/regress/regress0/smtlib/define-fun-rec-logic.smt2 new file mode 100644 index 000000000..1af16210d --- /dev/null +++ b/test/regress/regress0/smtlib/define-fun-rec-logic.smt2 @@ -0,0 +1,12 @@ +; EXPECT: unsat +; EXPECT: (error "recursive function definitions require a logic with quantifiers") +; EXIT: 1 +(set-logic UFBV) +(define-funs-rec ((f ((b Bool)) Bool) (g ((b Bool)) Bool)) (b b)) +(assert (g false)) +(check-sat) +(reset) +(set-logic QF_BV) +(define-funs-rec ((f ((b Bool)) Bool) (g ((b Bool)) Bool)) (b b)) +(assert (g false)) +(check-sat) diff --git a/test/regress/regress0/smtlib/issue4552.smt2 b/test/regress/regress0/smtlib/issue4552.smt2 new file mode 100644 index 000000000..af8e0b948 --- /dev/null +++ b/test/regress/regress0/smtlib/issue4552.smt2 @@ -0,0 +1,27 @@ +; COMMAND-LINE: --incremental +; EXPECT: unsat +; EXPECT: unsat +; EXPECT: unsat +(set-logic UF) +(set-option :global-declarations true) + +(push) +(define a true) +(define (f (b Bool)) b) +(define-const a2 Bool true) + +(define-fun a3 () Bool true) + +(define-fun-rec b () Bool true) +(define-funs-rec ((g ((b Bool)) Bool)) (b)) +(assert (or (not a) (not a2) (not a3) (not b) (g false))) +(check-sat) +(pop) + +(assert (or (not a) (not a2) (not a3) (not b) (g false))) +(check-sat) + +(reset-assertions) + +(assert (or (not a) (not a2) (not a3) (not b) (g false))) +(check-sat) diff --git a/test/regress/regress0/strings/issue4662-consume-nterm.smt2 b/test/regress/regress0/strings/issue4662-consume-nterm.smt2 new file mode 100644 index 000000000..a87279b4c --- /dev/null +++ b/test/regress/regress0/strings/issue4662-consume-nterm.smt2 @@ -0,0 +1,6 @@ +(set-logic QF_S) +(set-info :status unsat) +(declare-fun a () String) +(define-fun b () RegLan (str.to_re "A")) +(assert (str.in_re (str.++ "B" a) (re.+ (re.++ (re.opt b) (re.opt b))))) +(check-sat) diff --git a/test/regress/regress0/strings/issue4674-recomp-nf.smt2 b/test/regress/regress0/strings/issue4674-recomp-nf.smt2 new file mode 100644 index 000000000..2096d51ef --- /dev/null +++ b/test/regress/regress0/strings/issue4674-recomp-nf.smt2 @@ -0,0 +1,5 @@ +(set-logic QF_S) +(set-info :status sat) +(declare-fun a () String) +(assert (str.in_re "" (re.++ (str.to_re a) (re.comp re.allchar)))) +(check-sat) diff --git a/test/regress/regress0/sygus/pLTL-sygus-syntax-err.sy b/test/regress/regress0/sygus/pLTL-sygus-syntax-err.sy index 1b5690d3a..848ae0349 100644 --- a/test/regress/regress0/sygus/pLTL-sygus-syntax-err.sy +++ b/test/regress/regress0/sygus/pLTL-sygus-syntax-err.sy @@ -1,10 +1,10 @@ ; REQUIRES: no-competition ; COMMAND-LINE: --sygus-out=status --sygus-rec-fun --lang=sygus2 -; EXPECT-ERROR: CVC4 Error: -; EXPECT-ERROR: Parse Error: pLTL-sygus-syntax-err.sy:80.19: number of arguments does not match the constructor type +; EXPECT-ERROR: (error "Parse Error: pLTL-sygus-syntax-err.sy:80.19: number of arguments does not match the constructor type ; EXPECT-ERROR: ; EXPECT-ERROR: (Op2 <O2> <F>) ; EXPECT-ERROR: ^ +; EXPECT-ERROR: ") ; EXIT: 1 (set-logic ALL) (set-option :lang sygus2) diff --git a/test/regress/regress0/uf/issue4446.smt2 b/test/regress/regress0/uf/issue4446.smt2 new file mode 100644 index 000000000..e59c3ee10 --- /dev/null +++ b/test/regress/regress0/uf/issue4446.smt2 @@ -0,0 +1,7 @@ +(set-logic QF_AUFLIA) +(declare-fun a (Bool) Bool) +(declare-fun b () Bool) +(declare-fun c () Bool) +(assert (or (a b) (a c))) +(set-info :status sat) +(check-sat) diff --git a/test/regress/regress0/unconstrained/4481.smt2 b/test/regress/regress0/unconstrained/4481.smt2 index 028607093..19179f4d7 100644 --- a/test/regress/regress0/unconstrained/4481.smt2 +++ b/test/regress/regress0/unconstrained/4481.smt2 @@ -1,5 +1,6 @@ ; COMMAND-LINE: --unconstrained-simp -; EXPECT: unsat +; EXPECT: (error "Cannot use unconstrained simplification in this logic, due to (possibly internally introduced) quantified formula.") +; EXIT: 1 (set-logic ALL) (set-info :status unsat) (declare-fun a () Int) diff --git a/test/regress/regress0/unconstrained/4484.smt2 b/test/regress/regress0/unconstrained/4484.smt2 deleted file mode 100644 index f2f11295b..000000000 --- a/test/regress/regress0/unconstrained/4484.smt2 +++ /dev/null @@ -1,8 +0,0 @@ -; COMMAND-LINE: --unconstrained-simp -; EXPECT: unsat -(set-logic QF_NIRA) -(set-info :status unsat) -(declare-fun a () Real) -(assert (= (to_int a) 2)) -(assert (= (to_int (/ a 2.0)) 2)) -(check-sat) diff --git a/test/regress/regress0/unconstrained/4486.smt2 b/test/regress/regress0/unconstrained/4486.smt2 deleted file mode 100644 index 01771ce66..000000000 --- a/test/regress/regress0/unconstrained/4486.smt2 +++ /dev/null @@ -1,8 +0,0 @@ -; COMMAND-LINE: --unconstrained-simp -; EXPECT: sat -(set-logic ALL) -(set-info :status sat) -(declare-fun x () Real) -(assert (is_int x)) -(assert (is_int (+ x 1))) -(check-sat) diff --git a/test/regress/regress0/unconstrained/issue4644.smt2 b/test/regress/regress0/unconstrained/issue4644.smt2 new file mode 100644 index 000000000..aeb2bfc84 --- /dev/null +++ b/test/regress/regress0/unconstrained/issue4644.smt2 @@ -0,0 +1,9 @@ +; COMMAND-LINE: --unconstrained-simp +(set-logic ALL) +(declare-fun a () Bool) +(declare-fun b () Bool) +(declare-fun c () Bool) +(assert (distinct a c)) +(assert (= a b (= b c))) +(set-info :status sat) +(check-sat) |