summaryrefslogtreecommitdiff
path: root/test/regress/regress0/push-pop/arith
diff options
context:
space:
mode:
Diffstat (limited to 'test/regress/regress0/push-pop/arith')
-rw-r--r--test/regress/regress0/push-pop/arith/fuzz_3_1.smt21
-rw-r--r--test/regress/regress0/push-pop/arith/fuzz_3_10.smt21
-rw-r--r--test/regress/regress0/push-pop/arith/fuzz_3_11.smt21
-rw-r--r--test/regress/regress0/push-pop/arith/fuzz_3_12.smt21
-rw-r--r--test/regress/regress0/push-pop/arith/fuzz_3_13.smt21
-rw-r--r--test/regress/regress0/push-pop/arith/fuzz_3_14.smt21
-rw-r--r--test/regress/regress0/push-pop/arith/fuzz_3_15.smt21
-rw-r--r--test/regress/regress0/push-pop/arith/fuzz_3_2.smt21
-rw-r--r--test/regress/regress0/push-pop/arith/fuzz_3_3.smt21
-rw-r--r--test/regress/regress0/push-pop/arith/fuzz_3_4.smt21
-rw-r--r--test/regress/regress0/push-pop/arith/fuzz_3_5.smt21
-rw-r--r--test/regress/regress0/push-pop/arith/fuzz_3_6.smt21
-rw-r--r--test/regress/regress0/push-pop/arith/fuzz_3_7.smt21
-rw-r--r--test/regress/regress0/push-pop/arith/fuzz_3_8.smt21
-rw-r--r--test/regress/regress0/push-pop/arith/fuzz_3_9.smt21
-rw-r--r--test/regress/regress0/push-pop/arith/fuzz_5_1.smt21
-rw-r--r--test/regress/regress0/push-pop/arith/fuzz_5_2.smt21
-rw-r--r--test/regress/regress0/push-pop/arith/fuzz_5_3.smt21
-rw-r--r--test/regress/regress0/push-pop/arith/fuzz_5_4.smt21
-rw-r--r--test/regress/regress0/push-pop/arith/fuzz_5_5.smt21
-rw-r--r--test/regress/regress0/push-pop/arith/fuzz_5_6.smt21
21 files changed, 0 insertions, 21 deletions
diff --git a/test/regress/regress0/push-pop/arith/fuzz_3_1.smt2 b/test/regress/regress0/push-pop/arith/fuzz_3_1.smt2
index 73399358a..bf2d2a8c3 100644
--- a/test/regress/regress0/push-pop/arith/fuzz_3_1.smt2
+++ b/test/regress/regress0/push-pop/arith/fuzz_3_1.smt2
@@ -3,7 +3,6 @@
; EXPECT: sat
; EXPECT: unsat
; EXPECT: sat
-; EXIT: 10
(set-logic QF_LRA)
(declare-fun x0 () Real)
(declare-fun x1 () Real)
diff --git a/test/regress/regress0/push-pop/arith/fuzz_3_10.smt2 b/test/regress/regress0/push-pop/arith/fuzz_3_10.smt2
index cdd6a6b18..389c91573 100644
--- a/test/regress/regress0/push-pop/arith/fuzz_3_10.smt2
+++ b/test/regress/regress0/push-pop/arith/fuzz_3_10.smt2
@@ -2,7 +2,6 @@
; EXPECT: sat
; EXPECT: unsat
; EXPECT: sat
-; EXIT: 10
(set-logic QF_LRA)
(declare-fun x0 () Real)
(declare-fun x1 () Real)
diff --git a/test/regress/regress0/push-pop/arith/fuzz_3_11.smt2 b/test/regress/regress0/push-pop/arith/fuzz_3_11.smt2
index 9078acf46..81fe3b046 100644
--- a/test/regress/regress0/push-pop/arith/fuzz_3_11.smt2
+++ b/test/regress/regress0/push-pop/arith/fuzz_3_11.smt2
@@ -5,7 +5,6 @@
; EXPECT: sat
; EXPECT: unsat
; EXPECT: sat
-; EXIT: 10
(set-logic QF_LRA)
(declare-fun x0 () Real)
(declare-fun x1 () Real)
diff --git a/test/regress/regress0/push-pop/arith/fuzz_3_12.smt2 b/test/regress/regress0/push-pop/arith/fuzz_3_12.smt2
index f3d6d95de..d797c1897 100644
--- a/test/regress/regress0/push-pop/arith/fuzz_3_12.smt2
+++ b/test/regress/regress0/push-pop/arith/fuzz_3_12.smt2
@@ -8,7 +8,6 @@
; EXPECT: sat
; EXPECT: unsat
; EXPECT: sat
-; EXIT: 10
(set-logic QF_LRA)
(declare-fun x0 () Real)
(declare-fun x1 () Real)
diff --git a/test/regress/regress0/push-pop/arith/fuzz_3_13.smt2 b/test/regress/regress0/push-pop/arith/fuzz_3_13.smt2
index ff78a7d39..2e4b9d2b8 100644
--- a/test/regress/regress0/push-pop/arith/fuzz_3_13.smt2
+++ b/test/regress/regress0/push-pop/arith/fuzz_3_13.smt2
@@ -6,7 +6,6 @@
; EXPECT: sat
; EXPECT: sat
; EXPECT: sat
-; EXIT: 10
(set-logic QF_LRA)
(declare-fun x0 () Real)
(declare-fun x1 () Real)
diff --git a/test/regress/regress0/push-pop/arith/fuzz_3_14.smt2 b/test/regress/regress0/push-pop/arith/fuzz_3_14.smt2
index 01191c4da..0399bbffa 100644
--- a/test/regress/regress0/push-pop/arith/fuzz_3_14.smt2
+++ b/test/regress/regress0/push-pop/arith/fuzz_3_14.smt2
@@ -5,7 +5,6 @@
; EXPECT: sat
; EXPECT: unsat
; EXPECT: sat
-; EXIT: 10
(set-logic QF_LRA)
(declare-fun x0 () Real)
(declare-fun x1 () Real)
diff --git a/test/regress/regress0/push-pop/arith/fuzz_3_15.smt2 b/test/regress/regress0/push-pop/arith/fuzz_3_15.smt2
index e4b824dcc..2a8ffe0fa 100644
--- a/test/regress/regress0/push-pop/arith/fuzz_3_15.smt2
+++ b/test/regress/regress0/push-pop/arith/fuzz_3_15.smt2
@@ -5,7 +5,6 @@
; EXPECT: sat
; EXPECT: sat
; EXPECT: sat
-; EXIT: 10
(set-logic QF_LRA)
(declare-fun x0 () Real)
(declare-fun x1 () Real)
diff --git a/test/regress/regress0/push-pop/arith/fuzz_3_2.smt2 b/test/regress/regress0/push-pop/arith/fuzz_3_2.smt2
index 3003fa52b..cbff796c6 100644
--- a/test/regress/regress0/push-pop/arith/fuzz_3_2.smt2
+++ b/test/regress/regress0/push-pop/arith/fuzz_3_2.smt2
@@ -6,7 +6,6 @@
; EXPECT: sat
; EXPECT: sat
; EXPECT: sat
-; EXIT: 10
(set-logic QF_LRA)
(declare-fun x0 () Real)
(declare-fun x1 () Real)
diff --git a/test/regress/regress0/push-pop/arith/fuzz_3_3.smt2 b/test/regress/regress0/push-pop/arith/fuzz_3_3.smt2
index c437a5fb8..ec072821c 100644
--- a/test/regress/regress0/push-pop/arith/fuzz_3_3.smt2
+++ b/test/regress/regress0/push-pop/arith/fuzz_3_3.smt2
@@ -3,7 +3,6 @@
; EXPECT: sat
; EXPECT: unsat
; EXPECT: sat
-; EXIT: 10
(set-logic QF_LRA)
(declare-fun x0 () Real)
(declare-fun x1 () Real)
diff --git a/test/regress/regress0/push-pop/arith/fuzz_3_4.smt2 b/test/regress/regress0/push-pop/arith/fuzz_3_4.smt2
index 4d42615f4..93be94865 100644
--- a/test/regress/regress0/push-pop/arith/fuzz_3_4.smt2
+++ b/test/regress/regress0/push-pop/arith/fuzz_3_4.smt2
@@ -3,7 +3,6 @@
; EXPECT: sat
; EXPECT: sat
; EXPECT: sat
-; EXIT: 10
(set-logic QF_LRA)
(declare-fun x0 () Real)
(declare-fun x1 () Real)
diff --git a/test/regress/regress0/push-pop/arith/fuzz_3_5.smt2 b/test/regress/regress0/push-pop/arith/fuzz_3_5.smt2
index a566eb1f3..fd9204081 100644
--- a/test/regress/regress0/push-pop/arith/fuzz_3_5.smt2
+++ b/test/regress/regress0/push-pop/arith/fuzz_3_5.smt2
@@ -7,7 +7,6 @@
; EXPECT: sat
; EXPECT: unsat
; EXPECT: sat
-; EXIT: 10
(set-logic QF_LRA)
(declare-fun x0 () Real)
(declare-fun x1 () Real)
diff --git a/test/regress/regress0/push-pop/arith/fuzz_3_6.smt2 b/test/regress/regress0/push-pop/arith/fuzz_3_6.smt2
index 7fcd67745..1901016c2 100644
--- a/test/regress/regress0/push-pop/arith/fuzz_3_6.smt2
+++ b/test/regress/regress0/push-pop/arith/fuzz_3_6.smt2
@@ -5,7 +5,6 @@
; EXPECT: unsat
; EXPECT: unsat
; EXPECT: sat
-; EXIT: 10
(set-logic QF_LRA)
(declare-fun x0 () Real)
(declare-fun x1 () Real)
diff --git a/test/regress/regress0/push-pop/arith/fuzz_3_7.smt2 b/test/regress/regress0/push-pop/arith/fuzz_3_7.smt2
index 88fd866de..c3b8aadc7 100644
--- a/test/regress/regress0/push-pop/arith/fuzz_3_7.smt2
+++ b/test/regress/regress0/push-pop/arith/fuzz_3_7.smt2
@@ -5,7 +5,6 @@
; EXPECT: sat
; EXPECT: unsat
; EXPECT: sat
-; EXIT: 10
(set-logic QF_LRA)
(declare-fun x0 () Real)
(declare-fun x1 () Real)
diff --git a/test/regress/regress0/push-pop/arith/fuzz_3_8.smt2 b/test/regress/regress0/push-pop/arith/fuzz_3_8.smt2
index 329be0391..cebf4d3e6 100644
--- a/test/regress/regress0/push-pop/arith/fuzz_3_8.smt2
+++ b/test/regress/regress0/push-pop/arith/fuzz_3_8.smt2
@@ -8,7 +8,6 @@
; EXPECT: sat
; EXPECT: sat
; EXPECT: sat
-; EXIT: 10
(set-logic QF_LRA)
(declare-fun x0 () Real)
(declare-fun x1 () Real)
diff --git a/test/regress/regress0/push-pop/arith/fuzz_3_9.smt2 b/test/regress/regress0/push-pop/arith/fuzz_3_9.smt2
index db180f3f4..96aaf9f51 100644
--- a/test/regress/regress0/push-pop/arith/fuzz_3_9.smt2
+++ b/test/regress/regress0/push-pop/arith/fuzz_3_9.smt2
@@ -8,7 +8,6 @@
; EXPECT: sat
; EXPECT: unsat
; EXPECT: sat
-; EXIT: 10
(set-logic QF_LRA)
(declare-fun x0 () Real)
(declare-fun x1 () Real)
diff --git a/test/regress/regress0/push-pop/arith/fuzz_5_1.smt2 b/test/regress/regress0/push-pop/arith/fuzz_5_1.smt2
index 9e61f7c4d..05414230a 100644
--- a/test/regress/regress0/push-pop/arith/fuzz_5_1.smt2
+++ b/test/regress/regress0/push-pop/arith/fuzz_5_1.smt2
@@ -8,7 +8,6 @@
; EXPECT: sat
; EXPECT: unsat
; EXPECT: sat
-; EXIT: 10
(set-logic QF_LRA)
(declare-fun x0 () Real)
(declare-fun x1 () Real)
diff --git a/test/regress/regress0/push-pop/arith/fuzz_5_2.smt2 b/test/regress/regress0/push-pop/arith/fuzz_5_2.smt2
index cfcd80a44..9c387d89f 100644
--- a/test/regress/regress0/push-pop/arith/fuzz_5_2.smt2
+++ b/test/regress/regress0/push-pop/arith/fuzz_5_2.smt2
@@ -8,7 +8,6 @@
; EXPECT: sat
; EXPECT: unsat
; EXPECT: sat
-; EXIT: 10
(set-logic QF_LRA)
(declare-fun x0 () Real)
(declare-fun x1 () Real)
diff --git a/test/regress/regress0/push-pop/arith/fuzz_5_3.smt2 b/test/regress/regress0/push-pop/arith/fuzz_5_3.smt2
index f79d3ee69..b61eb001f 100644
--- a/test/regress/regress0/push-pop/arith/fuzz_5_3.smt2
+++ b/test/regress/regress0/push-pop/arith/fuzz_5_3.smt2
@@ -7,7 +7,6 @@
; EXPECT: sat
; EXPECT: unsat
; EXPECT: sat
-; EXIT: 10
(set-logic QF_LRA)
(declare-fun x0 () Real)
(declare-fun x1 () Real)
diff --git a/test/regress/regress0/push-pop/arith/fuzz_5_4.smt2 b/test/regress/regress0/push-pop/arith/fuzz_5_4.smt2
index 95a64c578..5d46d281f 100644
--- a/test/regress/regress0/push-pop/arith/fuzz_5_4.smt2
+++ b/test/regress/regress0/push-pop/arith/fuzz_5_4.smt2
@@ -6,7 +6,6 @@
; EXPECT: unsat
; EXPECT: sat
; EXPECT: sat
-; EXIT: 10
(set-logic QF_LRA)
(declare-fun x0 () Real)
(declare-fun x1 () Real)
diff --git a/test/regress/regress0/push-pop/arith/fuzz_5_5.smt2 b/test/regress/regress0/push-pop/arith/fuzz_5_5.smt2
index 8b41d054c..72b2aa088 100644
--- a/test/regress/regress0/push-pop/arith/fuzz_5_5.smt2
+++ b/test/regress/regress0/push-pop/arith/fuzz_5_5.smt2
@@ -8,7 +8,6 @@
; EXPECT: sat
; EXPECT: unsat
; EXPECT: sat
-; EXIT: 10
(set-logic QF_LRA)
(declare-fun x0 () Real)
(declare-fun x1 () Real)
diff --git a/test/regress/regress0/push-pop/arith/fuzz_5_6.smt2 b/test/regress/regress0/push-pop/arith/fuzz_5_6.smt2
index 8da0aeb7e..1cffc92cb 100644
--- a/test/regress/regress0/push-pop/arith/fuzz_5_6.smt2
+++ b/test/regress/regress0/push-pop/arith/fuzz_5_6.smt2
@@ -8,7 +8,6 @@
; EXPECT: sat
; EXPECT: unsat
; EXPECT: sat
-; EXIT: 10
(set-logic QF_LRA)
(declare-fun x0 () Real)
(declare-fun x1 () Real)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback