diff options
Diffstat (limited to 'test')
25 files changed, 186 insertions, 17 deletions
diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am index 4ea78a826..f16e18bdf 100644 --- a/test/regress/regress0/Makefile.am +++ b/test/regress/regress0/Makefile.am @@ -47,6 +47,8 @@ SMT_TESTS = \ # Regression tests for SMT2 inputs SMT2_TESTS = \ arrayinuf_declare.smt2 \ + boolean-terms-kernel1.smt2 \ + boolean-terms-kernel2.smt2 \ chained-equality.smt2 \ ite2.smt2 \ ite3.smt2 \ diff --git a/test/regress/regress0/boolean-terms-kernel1.smt2 b/test/regress/regress0/boolean-terms-kernel1.smt2 new file mode 100644 index 000000000..a999a6a76 --- /dev/null +++ b/test/regress/regress0/boolean-terms-kernel1.smt2 @@ -0,0 +1,13 @@ +; COMMAND-LINE: --incremental +; EXPECT: sat +; EXPECT: sat +(set-logic QF_ABV) +(declare-fun b () (_ BitVec 32)) +(declare-fun hk () (Array Bool (_ BitVec 32))) +(push 1) +(assert (not (= b (select hk true)))) +(check-sat) +(pop 1) +(assert (not (= b (_ bv0 32)))) +(assert (= b (select hk true))) +(check-sat) diff --git a/test/regress/regress0/boolean-terms-kernel2.smt2 b/test/regress/regress0/boolean-terms-kernel2.smt2 new file mode 100644 index 000000000..a4e49dd90 --- /dev/null +++ b/test/regress/regress0/boolean-terms-kernel2.smt2 @@ -0,0 +1,19 @@ +; COMMAND-LINE: --incremental +; EXPECT: unsat +; EXPECT: sat +(set-logic QF_ABV) +(declare-fun b () Bool) +(declare-fun c () Bool) +(declare-fun a () (Array Bool (Array (_ BitVec 32) (_ BitVec 32)))) +(declare-fun v2 () (_ BitVec 32)) +(declare-fun r0 () (_ BitVec 32)) +(declare-fun r1 () (_ BitVec 32)) +(declare-fun l () (_ BitVec 32)) +(declare-fun i () (_ BitVec 32)) +(assert c) +(push 1) +(assert (not (=> false (not (= i (select (select a true) (bvsub (bvmul (bvsdiv v2 (_ bv2 32)) (bvadd (bvmul (_ bv2 32) l) (_ bv1 32))) (_ bv1 32)))))))) +(check-sat) +(pop 1) +(assert (not (=> (= i (select (select a true) (bvsub (bvmul (bvsdiv v2 (_ bv2 32)) (bvadd (bvmul (_ bv2 32) l) (_ bv1 32))) (_ bv1 32)))) (not (= r1 (ite b i r0)))))) +(check-sat) diff --git a/test/regress/regress0/bug548a.smt2 b/test/regress/regress0/bug548a.smt2 index 12658e507..75d82d98f 100644 --- a/test/regress/regress0/bug548a.smt2 +++ b/test/regress/regress0/bug548a.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --rewrite-divk --tlimit 1000 ; EXPECT: unknown -(set-logic LIA) +(set-logic AUFLIA) (declare-fun f (Int) Int) diff --git a/test/regress/regress0/sets/Makefile.am b/test/regress/regress0/sets/Makefile.am index 32a96ec21..fe53838be 100644 --- a/test/regress/regress0/sets/Makefile.am +++ b/test/regress/regress0/sets/Makefile.am @@ -53,6 +53,8 @@ TESTS = \ jan28/TalkingAboutSets.hs.fqout.3577minimized.smt2 \ sets-sample.smt2 \ eqtest.smt2 \ + mar2014/lemmabug-ListElts317minimized.smt2 \ + mar2014/sharing-preregister.smt2 \ emptyset.smt2 \ error2.smt2 diff --git a/test/regress/regress0/sets/error1.smt2 b/test/regress/regress0/sets/error1.smt2 index c4b3dd551..1241b117f 100644 --- a/test/regress/regress0/sets/error1.smt2 +++ b/test/regress/regress0/sets/error1.smt2 @@ -1,4 +1,3 @@ -; COMMAND-LINE: --no-check-models ; EXPECT: sat (set-logic QF_UFLIA_SETS) (set-info :status sat) diff --git a/test/regress/regress0/sets/feb3/ListElts.hs.fqout.cvc4.317.smt2 b/test/regress/regress0/sets/feb3/ListElts.hs.fqout.cvc4.317.smt2 index 290ee95d5..7a8661e4d 100644 --- a/test/regress/regress0/sets/feb3/ListElts.hs.fqout.cvc4.317.smt2 +++ b/test/regress/regress0/sets/feb3/ListElts.hs.fqout.cvc4.317.smt2 @@ -1,4 +1,3 @@ -; COMMAND-LINE: --no-check-models ; EXPECT: sat (set-logic QF_ALL_SUPPORTED) (set-info :status sat) diff --git a/test/regress/regress0/sets/jan27/deepmeas0.hs.fqout.cvc4.41.smt2 b/test/regress/regress0/sets/jan27/deepmeas0.hs.fqout.cvc4.41.smt2 index bcc4c33da..0aa6c88ae 100644 --- a/test/regress/regress0/sets/jan27/deepmeas0.hs.fqout.cvc4.41.smt2 +++ b/test/regress/regress0/sets/jan27/deepmeas0.hs.fqout.cvc4.41.smt2 @@ -1,4 +1,3 @@ -; COMMAND-LINE: --no-check-models ; EXPECT: sat (set-logic QF_ALL_SUPPORTED) (set-info :status sat) diff --git a/test/regress/regress0/sets/jan28/TalkingAboutSets.hs.fqout.3577minimized.smt2 b/test/regress/regress0/sets/jan28/TalkingAboutSets.hs.fqout.3577minimized.smt2 index 5a44c0344..35110d831 100644 --- a/test/regress/regress0/sets/jan28/TalkingAboutSets.hs.fqout.3577minimized.smt2 +++ b/test/regress/regress0/sets/jan28/TalkingAboutSets.hs.fqout.3577minimized.smt2 @@ -1,4 +1,3 @@ -; COMMAND-LINE: --no-check-models ; EXPECT: sat (set-logic QF_ALL_SUPPORTED) (set-info :status sat) diff --git a/test/regress/regress0/sets/jan28/TalkingAboutSets.hs.fqout.cvc4.3577.smt2 b/test/regress/regress0/sets/jan28/TalkingAboutSets.hs.fqout.cvc4.3577.smt2 index 67d64bd05..d0fda8b86 100644 --- a/test/regress/regress0/sets/jan28/TalkingAboutSets.hs.fqout.cvc4.3577.smt2 +++ b/test/regress/regress0/sets/jan28/TalkingAboutSets.hs.fqout.cvc4.3577.smt2 @@ -1,4 +1,3 @@ -; COMMAND-LINE: --no-check-models ; EXPECT: sat (set-logic QF_ALL_SUPPORTED) (set-info :status sat) diff --git a/test/regress/regress0/sets/mar2014/lemmabug-ListElts317minimized.smt2 b/test/regress/regress0/sets/mar2014/lemmabug-ListElts317minimized.smt2 new file mode 100644 index 000000000..1ea3ea6b5 --- /dev/null +++ b/test/regress/regress0/sets/mar2014/lemmabug-ListElts317minimized.smt2 @@ -0,0 +1,89 @@ +; EXPECT: sat + +; Observed behavior: +; --check-model failed for set-term (union (z3f69 z3v151) (setenum z3v143)) +; with different set of elements in the model for representative and the node +; itself. +; +; Issue: +; The trouble with data structure being mainted to ensure that things +; for which lemmas have been generated are not generated again. This +; data structure (d_pendingEverInserted) needs to be user context +; dependent. The bug was in the sequence of steps from requesting that +; a lemma be generated to when it actually was. Sequence was: +; addToPending (and also adds to pending ever inserted) -> +; isComplete (might remove things from pending if requirment met in other ways) -> +; getLemma (actually generated the lemma, if requirement not already met) +; +; Resolution: +; adding terms to d_pendingEverInserted was moved from addToPending() +; to getLemma(). + +(set-logic QF_ALL_SUPPORTED) +(set-info :status sat) +(define-sort Elt () Int) +(define-sort mySet () (Set Elt )) +(define-fun smt_set_emp () mySet (as emptyset mySet)) +(define-fun smt_set_mem ((x Elt) (s mySet)) Bool (in x s)) +(define-fun smt_set_add ((s mySet) (x Elt)) mySet (union s (setenum x))) +(define-fun smt_set_cup ((s1 mySet) (s2 mySet)) mySet (union s1 s2)) +(define-fun smt_set_cap ((s1 mySet) (s2 mySet)) mySet (intersection s1 s2)) +;(define-fun smt_set_com ((s mySet)) mySet ((_ map not) s)) +(define-fun smt_set_dif ((s1 mySet) (s2 mySet)) mySet (setminus s1 s2)) +;(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (= smt_set_emp (smt_set_dif s1 s2))) +(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (subseteq s1 s2)) + +(declare-fun z3v58 () Int) +(declare-fun z3v59 () Int) +(assert (distinct z3v58 z3v59)) + +(declare-fun z3f60 (Int) Bool) +(declare-fun z3v61 () Int) +(declare-fun z3f62 (Int) Int) +(declare-fun z3v63 () Int) +(declare-fun z3v64 () Int) +(declare-fun z3v67 () Int) +(declare-fun z3f68 (Int) Int) +(declare-fun z3f69 (Int) mySet) +(declare-fun z3f70 (Int) mySet) +(declare-fun z3f71 (Int) Bool) +(declare-fun z3v90 () Int) +(declare-fun z3v91 () Int) +(declare-fun z3f92 (Int Int) Int) +(declare-fun z3v140 () Int) +(declare-fun z3v141 () Int) +(declare-fun z3v142 () Int) +(declare-fun z3v143 () Int) +(declare-fun z3v144 () Int) +(declare-fun z3v145 () Int) +(declare-fun z3v147 () Int) +(declare-fun z3v150 () Int) +(declare-fun z3v151 () Int) +(declare-fun z3v152 () Int) + +(assert (not (= (z3f69 z3v152) + (z3f69 z3v140)))) + +(assert (= (z3f69 z3v151) + (smt_set_cup (z3f69 z3v141) + (z3f69 z3v140)))) + +(assert (= (z3f69 z3v152) + (smt_set_cup (setenum z3v143) (z3f69 z3v151)))) + +(assert (= (z3f70 z3v152) + (smt_set_cup (setenum z3v143) (z3f70 z3v151)))) + +(assert (and + (= (z3f69 z3v142) + (smt_set_cup (setenum z3v143) (z3f69 z3v141))) + (= (z3f70 z3v142) + (smt_set_cup (setenum z3v143) (z3f70 z3v141))) + (= z3v142 (z3f92 z3v143 z3v141)) + (= z3v142 z3v144) + (= (z3f62 z3v61) z3v61) + (= (z3f62 z3v63) z3v63) + ) + ) + +(check-sat) diff --git a/test/regress/regress0/sets/mar2014/sharing-preregister.smt2 b/test/regress/regress0/sets/mar2014/sharing-preregister.smt2 new file mode 100644 index 000000000..dc42abfa2 --- /dev/null +++ b/test/regress/regress0/sets/mar2014/sharing-preregister.smt2 @@ -0,0 +1,12 @@ +; EXPECT: unsat +(set-logic QF_UFLIA_SETS) +(set-info :status sat) +(declare-fun a () Int) +(declare-fun b () Int) +(declare-fun x () (Set Int)) +(declare-fun y () (Set Int)) +(assert (= x (setenum a))) +(assert (= y (setenum b))) +(assert (not (= x y))) +(assert (and (< 1 a) (< a 3) (< 1 b) (< b 3))) +(check-sat) diff --git a/test/regress/regress0/sets/mar2014/stacks0.hs.78.cvc4.smt2 b/test/regress/regress0/sets/mar2014/stacks0.hs.78.cvc4.smt2 new file mode 100644 index 000000000..70c0057f9 --- /dev/null +++ b/test/regress/regress0/sets/mar2014/stacks0.hs.78.cvc4.smt2 @@ -0,0 +1 @@ +; PLACEHOLDER: benchmark to be added diff --git a/test/regress/regress0/sets/sets-new.smt2 b/test/regress/regress0/sets/sets-new.smt2 index c85ae4837..accb09799 100644 --- a/test/regress/regress0/sets/sets-new.smt2 +++ b/test/regress/regress0/sets/sets-new.smt2 @@ -1,4 +1,3 @@ -; COMMAND-LINE: --no-check-models ; EXPECT: sat (set-logic ALL_SUPPORTED) (set-info :status sat) diff --git a/test/regress/regress0/sets/sets-testlemma-ints.smt2 b/test/regress/regress0/sets/sets-testlemma-ints.smt2 new file mode 100644 index 000000000..9dd257401 --- /dev/null +++ b/test/regress/regress0/sets/sets-testlemma-ints.smt2 @@ -0,0 +1,7 @@ +; EXPECT: sat +(set-logic QF_UFLIA_SETS) +(set-info :status sat) +(declare-fun x () (Set Int)) +(declare-fun y () (Set Int)) +(assert (not (= x y))) +(check-sat) diff --git a/test/regress/regress0/sets/sets-testlemma-reals.smt2 b/test/regress/regress0/sets/sets-testlemma-reals.smt2 new file mode 100644 index 000000000..16e7780b4 --- /dev/null +++ b/test/regress/regress0/sets/sets-testlemma-reals.smt2 @@ -0,0 +1,7 @@ +; EXPECT: sat +(set-logic QF_UFLRA_SETS) +(set-info :status sat) +(declare-fun x () (Set Real)) +(declare-fun y () (Set Real)) +(assert (not (= x y))) +(check-sat) diff --git a/test/regress/regress0/sets/sets-testlemma.smt2 b/test/regress/regress0/sets/sets-testlemma.smt2 index 74ce72747..183f54242 100644 --- a/test/regress/regress0/sets/sets-testlemma.smt2 +++ b/test/regress/regress0/sets/sets-testlemma.smt2 @@ -1,6 +1,5 @@ -; COMMAND-LINE: --no-check-models ; EXPECT: sat -(set-logic QF_UFLIA_SETS) +(set-logic QF_UFBV_SETS) (set-info :status sat) (declare-fun x () (Set (_ BitVec 2))) (declare-fun y () (Set (_ BitVec 2))) diff --git a/test/regress/regress0/sets/sets-union.smt2 b/test/regress/regress0/sets/sets-union.smt2 index 6f6d3e019..656a0bc88 100644 --- a/test/regress/regress0/sets/sets-union.smt2 +++ b/test/regress/regress0/sets/sets-union.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --incremental --no-check-model +; COMMAND-LINE: --incremental ; EXPECT: sat ; EXPECT: unsat (set-logic ALL_SUPPORTED) diff --git a/test/regress/regress0/sets/union-1a-flip.smt2 b/test/regress/regress0/sets/union-1a-flip.smt2 index 59c2a2024..7bbe442e1 100644 --- a/test/regress/regress0/sets/union-1a-flip.smt2 +++ b/test/regress/regress0/sets/union-1a-flip.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --incremental --no-check-models +; COMMAND-LINE: --incremental ; EXPECT: unsat ; EXPECT: sat diff --git a/test/regress/regress0/sets/union-1b-flip.smt2 b/test/regress/regress0/sets/union-1b-flip.smt2 index 86fed459b..72c544553 100644 --- a/test/regress/regress0/sets/union-1b-flip.smt2 +++ b/test/regress/regress0/sets/union-1b-flip.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --incremental --no-check-models +; COMMAND-LINE: --incremental ; EXPECT: unsat ; EXPECT: sat diff --git a/test/regress/regress0/sets/union-2.smt2 b/test/regress/regress0/sets/union-2.smt2 index 32d949a53..e5e96be5a 100644 --- a/test/regress/regress0/sets/union-2.smt2 +++ b/test/regress/regress0/sets/union-2.smt2 @@ -1,4 +1,3 @@ -; COMMAND-LINE: --no-check-models ; EXPECT: sat (set-logic ALL_SUPPORTED) (set-info :status sat) diff --git a/test/regress/regress0/strings/Makefile.am b/test/regress/regress0/strings/Makefile.am index e82076520..9977da6a5 100644 --- a/test/regress/regress0/strings/Makefile.am +++ b/test/regress/regress0/strings/Makefile.am @@ -44,13 +44,13 @@ TESTS = \ loop006.smt2 \ loop007.smt2 \ loop008.smt2 \ - loop009.smt2 - -#regexp002.smt2 + loop009.smt2 \ + reloop.smt2 FAILING_TESTS = EXTRA_DIST = $(TESTS) \ + regexp002.smt2 \ type002.smt2 # and make sure to distribute it diff --git a/test/regress/regress0/strings/reloop.smt2 b/test/regress/regress0/strings/reloop.smt2 new file mode 100644 index 000000000..f54607121 --- /dev/null +++ b/test/regress/regress0/strings/reloop.smt2 @@ -0,0 +1,17 @@ +(set-logic QF_S)
+(set-info :status sat)
+
+(declare-fun x () String)
+(declare-fun y () String)
+(declare-fun z () String)
+(declare-fun w () String)
+
+(assert (str.in.re x (re.loop (str.to.re "a") 5)))
+(assert (str.in.re y (re.loop (str.to.re "b") 2 5)))
+(assert (str.in.re z (re.loop (str.to.re "c") 5)))
+(assert (> (str.len z) 7))
+(assert (str.in.re w (re.loop (str.to.re "b") 2 7)))
+(assert (> (str.len w) 2))
+(assert (< (str.len w) 5))
+
+(check-sat)
diff --git a/test/regress/regress0/strings/type002.smt2 b/test/regress/regress0/strings/type002.smt2 index ac4d9ab8a..cbad2226a 100644 --- a/test/regress/regress0/strings/type002.smt2 +++ b/test/regress/regress0/strings/type002.smt2 @@ -8,7 +8,7 @@ (declare-fun i () Int)
(assert (>= i 420))
-(assert (= x (int.to.str i)))
+(assert (= x (u16.to.str i)))
(assert (= x (str.++ y "0" z)))
(assert (not (= y "")))
(assert (not (= z "")))
diff --git a/test/unit/util/integer_black.h b/test/unit/util/integer_black.h index 48f32a307..de5669c11 100644 --- a/test/unit/util/integer_black.h +++ b/test/unit/util/integer_black.h @@ -24,6 +24,7 @@ using namespace CVC4; using namespace std; const char* largeVal = "4547897890548754897897897897890789078907890"; +const char* lotsOfLeadingZeroes = "00000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000001"; class IntegerBlack : public CxxTest::TestSuite { @@ -462,4 +463,11 @@ public: TS_ASSERT_EQUALS( r, Integer(-1)); } + + void testLeadingZeroes() { + string leadingZeroes(lotsOfLeadingZeroes); + Integer one(1u); + Integer one_from_string(leadingZeroes,2); + TS_ASSERT_EQUALS(one, one_from_string); + } }; |