From: Kshitij Bansal <kshitij@cs.nyu.edu>
Date: Wed, 12 Mar 2014 03:47:33 +0000 (-0400)
Subject: enable check-models for sets/ regressions
X-Git-Tag: cvc5-1.0.0~7002^2~7
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=705d2851e21fdac11005951f6a47a5446bc8e48b;p=cvc5.git

enable check-models for sets/ regressions
---

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/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.smt2 b/test/regress/regress0/sets/sets-testlemma.smt2
index 6f80b7147..183f54242 100644
--- a/test/regress/regress0/sets/sets-testlemma.smt2
+++ b/test/regress/regress0/sets/sets-testlemma.smt2
@@ -1,4 +1,3 @@
-; COMMAND-LINE: --no-check-models
 ; EXPECT: sat
 (set-logic QF_UFBV_SETS)
 (set-info :status sat)
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)