Merge remote-tracking branch 'upstream/master' into sets

17 files changed, 126 insertions, 14 deletions

diff --git a/test/regress/regress0/bug512.smt2 b/test/regress/regress0/bug512.smt2
index b0c970f37..1c8a0626a 100644
--- a/test/regress/regress0/bug512.smt2
+++ b/test/regress/regress0/bug512.smt2
@@ -1,6 +1,6 @@
 ; COMMAND-LINE: --tlimit-per 2500 -iq
 ; EXPECT: unknown
-; EXPECT: (:reason-unknown timeout)
+; EXPECT: (:reason-unknown incomplete)
 ; EXPECT: unsat
 (set-option :print-success false)
 (set-info :smt-lib-version 2.0)
diff --git a/test/regress/regress0/datatypes/Makefile.am b/test/regress/regress0/datatypes/Makefile.am
index 84adb4f84..e8a8f16f5 100644
--- a/test/regress/regress0/datatypes/Makefile.am
+++ b/test/regress/regress0/datatypes/Makefile.am
@@ -31,7 +31,6 @@ TESTS =	\
 	datatype0.cvc \
 	datatype1.cvc \
 	datatype2.cvc \
-	datatype3.cvc \
 	datatype4.cvc \
 	datatype13.cvc \
 	empty_tuprec.cvc \
@@ -64,6 +63,8 @@ TESTS =	\
 FAILING_TESTS = \
 	datatype-dump.cvc
 
+# takes a long time to build model on debug : datatype3.cvc
+
 EXTRA_DIST = $(TESTS)
 
 if CVC4_BUILD_PROFILE_COMPETITION
diff --git a/test/regress/regress0/datatypes/datatype1.cvc b/test/regress/regress0/datatypes/datatype1.cvc
index 5172eeb48..3934959f1 100644
--- a/test/regress/regress0/datatypes/datatype1.cvc
+++ b/test/regress/regress0/datatypes/datatype1.cvc
@@ -1,4 +1,4 @@
-% EXPECT: valid
+% EXPECT: invalid
 
 DATATYPE
   tree = node(left : tree, right : tree) | leaf
diff --git a/test/regress/regress0/datatypes/datatype3.cvc b/test/regress/regress0/datatypes/datatype3.cvc
index 5f130b6ae..fff1a5dd7 100644
--- a/test/regress/regress0/datatypes/datatype3.cvc
+++ b/test/regress/regress0/datatypes/datatype3.cvc
@@ -1,4 +1,4 @@
-% EXPECT: valid
+% EXPECT: invalid
 
 DATATYPE
   tree = node(left : tree, right : tree) | leaf
diff --git a/test/regress/regress0/datatypes/wrong-sel-simp.cvc b/test/regress/regress0/datatypes/wrong-sel-simp.cvc
index 7455f809c..b0dbdc46e 100644
--- a/test/regress/regress0/datatypes/wrong-sel-simp.cvc
+++ b/test/regress/regress0/datatypes/wrong-sel-simp.cvc
@@ -1,4 +1,4 @@
-% EXPECT: valid
+% EXPECT: invalid
 DATATYPE
   nat = succ(pred : nat) | zero
 END;
diff --git a/test/regress/regress0/fmf/Arrow_Order-smtlib.778341.smt b/test/regress/regress0/fmf/Arrow_Order-smtlib.778341.smt
index 536bc241f..f62f057e4 100644
--- a/test/regress/regress0/fmf/Arrow_Order-smtlib.778341.smt
+++ b/test/regress/regress0/fmf/Arrow_Order-smtlib.778341.smt
@@ -1,4 +1,4 @@
-% COMMAND-LINE: --finite-model-find
+% COMMAND-LINE: --finite-model-find --mbqi=gen-ev
 % EXPECT: unsat
 (benchmark Isabelle
 :status sat
diff --git a/test/regress/regress0/fmf/Makefile.am b/test/regress/regress0/fmf/Makefile.am
index b9a87231f..e3bfd39b8 100644
--- a/test/regress/regress0/fmf/Makefile.am
+++ b/test/regress/regress0/fmf/Makefile.am
@@ -23,18 +23,24 @@ TESTS =	\
 	agree466.smt2 \
 	ALG008-1.smt2 \
 	german169.smt2 \
-	Hoare-z3.931718.smt \
 	QEpres-uf.855035.smt \
 	agree467.smt2 \
 	Arrow_Order-smtlib.778341.smt \
 	german73.smt2 \
 	PUZ001+1.smt2 \
 	refcount24.cvc.smt2 \
-	bug0909.smt2 \
-	fmf-bound-int.smt2
+	fmf-bound-int.smt2 \
+	fc-simple.smt2 \
+	fc-unsat-tot-2.smt2 \
+	fc-unsat-pent.smt2 \
+	fc-pigeonhole19.smt2 \
+	Hoare-z3.931718.smt
 
 EXTRA_DIST = $(TESTS)
 
+# disabled for now :
+#  bug0909.smt2
+
 #if CVC4_BUILD_PROFILE_COMPETITION
 #else
 #TESTS += \
diff --git a/test/regress/regress0/fmf/QEpres-uf.855035.smt b/test/regress/regress0/fmf/QEpres-uf.855035.smt
index 980e5fd49..2945c8f4d 100644
--- a/test/regress/regress0/fmf/QEpres-uf.855035.smt
+++ b/test/regress/regress0/fmf/QEpres-uf.855035.smt
@@ -1,4 +1,4 @@
-% COMMAND-LINE: --finite-model-find
+% COMMAND-LINE: --finite-model-find --mbqi=gen-ev
 % EXPECT: sat
 (benchmark Isabelle
 :status sat
diff --git a/test/regress/regress0/fmf/fc-pigeonhole19.smt2 b/test/regress/regress0/fmf/fc-pigeonhole19.smt2
new file mode 100755
index 000000000..15c36682c
--- /dev/null
+++ b/test/regress/regress0/fmf/fc-pigeonhole19.smt2
@@ -0,0 +1,20 @@
+(set-logic UFC)

+(set-info :status unsat)

+

+(declare-sort P 0)

+(declare-sort H 0)

+

+(declare-fun p () P)

+(declare-fun h () H)

+

+; pigeonhole using native cardinality constraints

+(assert (fmf.card p 19))

+(assert (not (fmf.card p 18)))

+(assert (fmf.card h 18))

+(assert (not (fmf.card h 17)))

+

+; each pigeon has different holes

+(declare-fun f (P) H)

+(assert (forall ((p1 P) (p2 P)) (=> (not (= p1 p2)) (not (= (f p1) (f p2))))))

+

+(check-sat)
\ No newline at end of file
diff --git a/test/regress/regress0/fmf/fc-simple.smt2 b/test/regress/regress0/fmf/fc-simple.smt2
new file mode 100755
index 000000000..d1fd2301c
--- /dev/null
+++ b/test/regress/regress0/fmf/fc-simple.smt2
@@ -0,0 +1,12 @@
+(set-logic QF_UFC)
+(set-info :status unsat)
+
+(declare-sort U 0)
+
+(declare-fun a () U)
+(declare-fun c () U)
+
+(assert (fmf.card c 2))
+(assert (not (fmf.card a 4)))
+
+(check-sat)
diff --git a/test/regress/regress0/fmf/fc-unsat-pent.smt2 b/test/regress/regress0/fmf/fc-unsat-pent.smt2
new file mode 100755
index 000000000..f1721cb04
--- /dev/null
+++ b/test/regress/regress0/fmf/fc-unsat-pent.smt2
@@ -0,0 +1,20 @@
+(set-logic QF_UFC)

+(set-info :status unsat)

+

+(declare-sort U 0)

+

+(declare-fun a () U)

+(declare-fun b () U)

+(declare-fun c () U)

+(declare-fun d () U)

+(declare-fun e () U)

+

+(assert (not (= a b)))

+(assert (not (= b c)))

+(assert (not (= c d)))

+(assert (not (= d e)))

+(assert (not (= e a)))

+

+(assert (fmf.card c 2))

+

+(check-sat)
\ No newline at end of file
diff --git a/test/regress/regress0/fmf/fc-unsat-tot-2.smt2 b/test/regress/regress0/fmf/fc-unsat-tot-2.smt2
new file mode 100755
index 000000000..d946974ed
--- /dev/null
+++ b/test/regress/regress0/fmf/fc-unsat-tot-2.smt2
@@ -0,0 +1,14 @@
+(set-logic UFC)

+(set-info :status unsat)

+

+(declare-sort U 0)

+

+(declare-fun a () U)

+(declare-fun b () U)

+(declare-fun c () U)

+

+(assert (not (fmf.card a 2)))

+

+(assert (forall ((x U)) (or (= x a) (= x b))))

+

+(check-sat)
\ No newline at end of file
diff --git a/test/regress/regress0/quantifiers/bug269.smt2 b/test/regress/regress0/quantifiers/bug269.smt2
index 0d5aedbb3..2e50030d1 100644
--- a/test/regress/regress0/quantifiers/bug269.smt2
+++ b/test/regress/regress0/quantifiers/bug269.smt2
@@ -1,3 +1,5 @@
+; COMMAND-LINE: --full-saturate-quant
+; EXPECT: unsat
 (set-logic LRA)
 (set-info :status unsat)
 (declare-fun x4 () Real)
diff --git a/test/regress/regress0/quantifiers/burns13.smt2 b/test/regress/regress0/quantifiers/burns13.smt2
index ad970a2b2..3424c161e 100644
--- a/test/regress/regress0/quantifiers/burns13.smt2
+++ b/test/regress/regress0/quantifiers/burns13.smt2
@@ -1,3 +1,5 @@
+; COMMAND-LINE: --full-saturate-quant --decision=internal
+; EXPECT: unsat
 (set-logic AUFLIA)
 (set-info :source | Burns mutual exclusion protocol. This is a benchmark of the haRVey theorem prover. It was translated to SMT-LIB by Leonardo  de Moura |)
 (set-info :smt-lib-version 2.0)
diff --git a/test/regress/regress0/rewriterules/Makefile.am b/test/regress/regress0/rewriterules/Makefile.am
index 3a3a097bd..31f99905c 100644
--- a/test/regress/regress0/rewriterules/Makefile.am
+++ b/test/regress/regress0/rewriterules/Makefile.am
@@ -23,16 +23,16 @@ MAKEFLAGS = -k
 # put it below in "TESTS +="
 TESTS =	\
 	length_trick.smt2 \
-	length_trick2.smt2 \
 	length_gen_020.smt2 \
 	datatypes.smt2 \
 	datatypes_sat.smt2 \
 	reachability_back_to_the_future.smt2 \
 	relation.smt2 \
 	simulate_rewriting.smt2 \
-	native_arrays.smt2
+	native_arrays.smt2 \
+	read5.smt2
 
-# reachability_bbttf_eT_arrays.smt2 set_A_new_fast_tableau-base.smt2 set_A_new_fast_tableau-base_sat.smt2
+# length_trick2.smt2 reachability_bbttf_eT_arrays.smt2 set_A_new_fast_tableau-base.smt2 set_A_new_fast_tableau-base_sat.smt2
 
 EXTRA_DIST = $(TESTS)
 
diff --git a/test/regress/regress0/rewriterules/read5.smt2 b/test/regress/regress0/rewriterules/read5.smt2
new file mode 100755
index 000000000..e66df7c7e
--- /dev/null
+++ b/test/regress/regress0/rewriterules/read5.smt2
@@ -0,0 +1,35 @@
+(set-logic AUF)
+(set-info :source |
+Translated from old SVC processor verification benchmarks.  Contact Clark
+Barrett at barrett@cs.nyu.edu for more information.
+
+This benchmark was automatically translated into SMT-LIB format from
+CVC format using CVC Lite
+|)
+(set-info :smt-lib-version 2.0)
+(set-info :category "crafted")
+(set-info :status unsat)
+(declare-sort Index 0)
+(declare-sort Element 0)(declare-sort Arr 0)(declare-fun aselect (Arr Index) Element)(declare-fun astore (Arr Index Element) Arr)(declare-fun k (Arr Arr) Index)
+(declare-fun a () Index)
+(declare-fun aaa () Index)
+(declare-fun aa () Index)
+(declare-fun S () Arr)
+(declare-fun vvv () Element)
+(declare-fun v () Element)
+(declare-fun vv () Element)
+(declare-fun bbb () Index)
+(declare-fun www () Element)
+(declare-fun bb () Index)
+(declare-fun ww () Element)
+(declare-fun b () Index)
+(declare-fun w () Element)
+(declare-fun SS () Arr)
+(assert (let ((?v_3 (ite (= a aa) false true)) (?v_4 (ite (= aa aaa) false true)) (?v_1 (astore (astore (astore S a v) aa vv) aaa vvv)) (?v_0 (astore S aaa vvv)) (?v_2 (astore S aa vv))) (not (ite (ite (ite (ite (= a aaa) false true) (ite ?v_3 ?v_4 false) false) (ite (= (astore (astore ?v_0 a v) aa vv) ?v_1) (ite (= (astore (astore ?v_0 aa vv) a v) ?v_1) (ite (= (astore (astore ?v_2 a v) aaa vvv) ?v_1) (= (astore (astore ?v_2 aaa vvv) a v) ?v_1) false) false) false) true) (ite (ite (= ?v_1 (astore (astore (astore S bbb www) bb ww) b w)) (ite (ite ?v_3 (ite ?v_4 (ite (ite (= aa b) false true) (ite (ite (= aa bb) false true) (ite (= aa bbb) false true) false) false) false) false) (= (aselect S aa) vv) true) true) (ite (= S (astore SS a v)) (= S (astore SS a (aselect S a))) true) false) false))))
+; rewrite rule definition of arrays theory
+(assert (forall ((?x Arr) (?i Index) (?j Index) (?e Element)) (! (=> (not (= ?i ?j)) (= (aselect (astore ?x ?i ?e) ?j) (aselect ?x ?j))) :rewrite-rule)))
+(assert (forall ((?x Arr) (?i Index) (?e Element)) (! (=> true (= (aselect (astore ?x ?i ?e) ?i) ?e)) :rewrite-rule)))
+(assert (forall ((?x Arr) (?y Arr)) (! (=> (not (= ?x ?y)) (not (= (aselect ?x (k ?x ?y)) (aselect ?y (k ?x ?y))))) :rewrite-rule)))
+(assert (forall ((?x Arr) (?y Arr)) (! (! (=> true (or (= ?x ?y) (not (= ?x ?y)))) :pattern (?x)) :rewrite-rule)))
+(assert (forall ((?x Arr) (?i Index) (?j Index) (?e Element)) (! (! (=> true (or (= ?i ?j) (not (= ?i ?j)))) :pattern ((aselect (astore ?x ?i ?e) ?j))) :rewrite-rule)))(check-sat)
+(exit)
diff --git a/test/regress/regress0/tptp/Makefile.am b/test/regress/regress0/tptp/Makefile.am
index e0c8a2b48..e9274d2ee 100644
--- a/test/regress/regress0/tptp/Makefile.am
+++ b/test/regress/regress0/tptp/Makefile.am
@@ -35,7 +35,6 @@ TESTS =	\
 	tff0.p \
 	tff0-arith.p \
 	ARI086$(equals)1.p \
-	BOO003-4.p \
 	DAT001$(equals)1.p \
 	KRS018+1.p \
 	KRS063+1.p \
@@ -62,6 +61,7 @@ TEST_DEPS_DIST = \
 EXTRA_DIST = $(TESTS) \
 	$(TEST_DEPS_DIST) \
 	BOO027-1.p \
+	BOO003-4.p \
 	MGT031-1.p \
 	NLP114-1.p \
 	SYN075+1.p