summaryrefslogtreecommitdiff
path: root/test
diff options
context:
space:
mode:
Diffstat (limited to 'test')
-rw-r--r--test/regress/regress0/Makefile.am2
-rw-r--r--test/regress/regress0/boolean-terms-kernel1.smt213
-rw-r--r--test/regress/regress0/boolean-terms-kernel2.smt219
-rw-r--r--test/regress/regress0/bug548a.smt22
-rw-r--r--test/regress/regress0/sets/Makefile.am2
-rw-r--r--test/regress/regress0/sets/error1.smt21
-rw-r--r--test/regress/regress0/sets/feb3/ListElts.hs.fqout.cvc4.317.smt21
-rw-r--r--test/regress/regress0/sets/jan27/deepmeas0.hs.fqout.cvc4.41.smt21
-rw-r--r--test/regress/regress0/sets/jan28/TalkingAboutSets.hs.fqout.3577minimized.smt21
-rw-r--r--test/regress/regress0/sets/jan28/TalkingAboutSets.hs.fqout.cvc4.3577.smt21
-rw-r--r--test/regress/regress0/sets/mar2014/lemmabug-ListElts317minimized.smt289
-rw-r--r--test/regress/regress0/sets/mar2014/sharing-preregister.smt212
-rw-r--r--test/regress/regress0/sets/mar2014/stacks0.hs.78.cvc4.smt21
-rw-r--r--test/regress/regress0/sets/sets-new.smt21
-rw-r--r--test/regress/regress0/sets/sets-testlemma-ints.smt27
-rw-r--r--test/regress/regress0/sets/sets-testlemma-reals.smt27
-rw-r--r--test/regress/regress0/sets/sets-testlemma.smt23
-rw-r--r--test/regress/regress0/sets/sets-union.smt22
-rw-r--r--test/regress/regress0/sets/union-1a-flip.smt22
-rw-r--r--test/regress/regress0/sets/union-1b-flip.smt22
-rw-r--r--test/regress/regress0/sets/union-2.smt21
-rw-r--r--test/regress/regress0/strings/Makefile.am6
-rw-r--r--test/regress/regress0/strings/reloop.smt217
-rw-r--r--test/regress/regress0/strings/type002.smt22
-rw-r--r--test/unit/util/integer_black.h8
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);
+ }
};
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback