enable check-models for sets/ regressions

diff --git a/test/regress/regress0/sets/error1.smt2 b/test/regress/regress0/sets/error1.smt2
index c4b3dd55185914689bd830df6e3c247699fb7c9f..1241b117ffc1e116842838ff029bed1d3ed04b28 100644 (file)
--- 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 290ee95d59483fb2c84c0501ab14cba94c1b87f5..7a8661e4d4337a928de07bac6613db7b9a5cd619 100644 (file)
--- 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 bcc4c33da253094b220c2fda634b1b5931b34262..0aa6c88ae5c562fc0fccf22e74790bc066b621b4 100644 (file)
--- 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 5a44c0344b3de8581dc6fad72d3051f33daedb9b..35110d831d4283d686140d3af77e5e9fab73a368 100644 (file)
--- 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 67d64bd0574570e40a8f55b0082e888fd7e5b298..d0fda8b869685f866e7fbe365d6c2cb1bab5d59d 100644 (file)
--- 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 c85ae4837b8145efa78627ce52294a54a2558a8a..accb09799532282a02158a794158c2aaecf0838c 100644 (file)
--- 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 6f80b71475cec0c5af45eb57f3da89c60a33a7d2..183f542425d37a6a29963c35a3213b963a2fbe46 100644 (file)
--- 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 6f6d3e01924d93ee40f4a2026ac30d30350e16c8..656a0bc88d0bd5095f3dda6647c707888a0f9c0a 100644 (file)
--- 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 59c2a20249ca01617463c82e9cb86d6e82802ea3..7bbe442e185f8ba3e9253d57df7590cfc5bc003b 100644 (file)
--- 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 86fed459b450efbe8e506997a11e06bb14133ec6..72c5445532c6b5bc5fc088011961cbb5aefc200b 100644 (file)
--- 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 32d949a531b82cc26d53c114a1b442f2c4862f7f..e5e96be5ac95b414b6fbe54a9e059111ddd8ee83 100644 (file)
--- 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)