Sharing work

8 files changed, 63 insertions, 86 deletions

diff --git a/test/regress/regress0/arith/integers/Makefile.am b/test/regress/regress0/arith/integers/Makefile.am
index 3d7f40c71..d0340616f 100644
--- a/test/regress/regress0/arith/integers/Makefile.am
+++ b/test/regress/regress0/arith/integers/Makefile.am
@@ -23,77 +23,7 @@ TESTS =	\
 	arith-int-017.cvc \
 	arith-int-018.cvc \
 	arith-int-019.cvc \
-	arith-int-020.cvc \
-	arith-int-021.cvc \
-	arith-int-023.cvc \
-	arith-int-024.cvc \
-	arith-int-025.cvc \
-	arith-int-026.cvc \
-	arith-int-027.cvc \
-	arith-int-028.cvc \
-	arith-int-029.cvc \
-	arith-int-030.cvc \
-	arith-int-031.cvc \
-	arith-int-032.cvc \
-	arith-int-033.cvc \
-	arith-int-034.cvc \
-	arith-int-035.cvc \
-	arith-int-036.cvc \
-	arith-int-037.cvc \
-	arith-int-038.cvc \
-	arith-int-039.cvc \
-	arith-int-040.cvc \
-	arith-int-041.cvc \
-	arith-int-044.cvc \
-	arith-int-045.cvc \
-	arith-int-046.cvc \
-	arith-int-048.cvc \
-	arith-int-049.cvc \
-	arith-int-051.cvc \
-	arith-int-052.cvc \
-	arith-int-053.cvc \
-	arith-int-054.cvc \
-	arith-int-055.cvc \
-	arith-int-056.cvc \
-	arith-int-057.cvc \
-	arith-int-058.cvc \
-	arith-int-059.cvc \
-	arith-int-060.cvc \
-	arith-int-061.cvc \
-	arith-int-062.cvc \
-	arith-int-063.cvc \
-	arith-int-064.cvc \
-	arith-int-065.cvc \
-	arith-int-066.cvc \
-	arith-int-067.cvc \
-	arith-int-068.cvc \
-	arith-int-069.cvc \
-	arith-int-070.cvc \
-	arith-int-071.cvc \
-	arith-int-072.cvc \
-	arith-int-073.cvc \
-	arith-int-074.cvc \
-	arith-int-075.cvc \
-	arith-int-076.cvc \
-	arith-int-077.cvc \
-	arith-int-078.cvc \
-	arith-int-079.cvc \
-	arith-int-080.cvc \
-	arith-int-081.cvc \
-	arith-int-083.cvc \
-	arith-int-085.cvc \
-	arith-int-086.cvc \
-	arith-int-087.cvc \
-	arith-int-088.cvc \
-	arith-int-089.cvc \
-	arith-int-090.cvc \
-	arith-int-091.cvc \
-	arith-int-092.cvc \
-	arith-int-093.cvc \
-	arith-int-094.cvc \
-	arith-int-095.cvc \
-	arith-int-096.cvc \
-	arith-int-099.cvc
+	arith-int-020.cvc 
 
 EXTRA_DIST = $(TESTS) \
 	arith-int-008.cvc \
diff --git a/test/regress/regress0/uflra/Makefile.am b/test/regress/regress0/uflra/Makefile.am
index 5199f2b62..377489ef7 100644
--- a/test/regress/regress0/uflra/Makefile.am
+++ b/test/regress/regress0/uflra/Makefile.am
@@ -6,15 +6,19 @@ MAKEFLAGS = -k
 # put it below in "TESTS +="
 
 # Regression tests for SMT inputs
-#SMT_TESTS = \
-#	pb_real_10_0100_10_10.smt \
-#	pb_real_10_0100_10_11.smt \
-#	pb_real_10_0100_10_15.smt \
-#	pb_real_10_0100_10_16.smt \
-#	pb_real_10_0100_10_19.smt \
-#	pb_real_10_0200_10_22.smt \
-#	pb_real_10_0200_10_26.smt \
-#	pb_real_10_0200_10_29.smt
+SMT_TESTS = \
+	simple.01.cvc \
+	simple.02.cvc \
+	simple.03.cvc \
+	simple.04.cvc \
+	pb_real_10_0100_10_10.smt \
+	pb_real_10_0100_10_11.smt \
+	pb_real_10_0100_10_15.smt \
+	pb_real_10_0100_10_16.smt \
+	pb_real_10_0100_10_19.smt \
+	pb_real_10_0200_10_22.smt \
+	pb_real_10_0200_10_26.smt \
+	pb_real_10_0200_10_29.smt 
 
 # Regression tests for SMT2 inputs
 SMT2_TESTS =
diff --git a/test/regress/regress0/uflra/simple.01.cvc b/test/regress/regress0/uflra/simple.01.cvc
new file mode 100644
index 000000000..8904192ce
--- /dev/null
+++ b/test/regress/regress0/uflra/simple.01.cvc
@@ -0,0 +1,6 @@
+% EXPECT: sat
+% EXIT: 10
+x, y: REAL;
+f: REAL -> REAL;
+
+CHECKSAT NOT (f(x) = f(y));
\ No newline at end of file
diff --git a/test/regress/regress0/uflra/simple.02.cvc b/test/regress/regress0/uflra/simple.02.cvc
new file mode 100644
index 000000000..a14ca8a1f
--- /dev/null
+++ b/test/regress/regress0/uflra/simple.02.cvc
@@ -0,0 +1,10 @@
+% EXPECT: unsat
+% EXIT: 20
+x, y: REAL;
+f: REAL -> REAL;
+
+ASSERT (x <= y);
+ASSERT (y <= x);
+ASSERT NOT (f(x) = f(y));
+
+CHECKSAT;
\ No newline at end of file
diff --git a/test/regress/regress0/uflra/simple.03.cvc b/test/regress/regress0/uflra/simple.03.cvc
new file mode 100644
index 000000000..1fdeed40a
--- /dev/null
+++ b/test/regress/regress0/uflra/simple.03.cvc
@@ -0,0 +1,12 @@
+% EXPECT: sat
+% EXIT: 10
+x1, y1, z1: REAL;
+x2, y2, z2: REAL;
+f: REAL -> REAL;
+g: (REAL, REAL) -> REAL;
+
+ASSERT (z1 = f(x1));
+ASSERT (z2 = f(y1));
+ASSERT NOT (g(z1, z2) = g(z2, y2));
+
+CHECKSAT;
\ No newline at end of file
diff --git a/test/regress/regress0/uflra/simple.04.cvc b/test/regress/regress0/uflra/simple.04.cvc
new file mode 100644
index 000000000..c9c226fa2
--- /dev/null
+++ b/test/regress/regress0/uflra/simple.04.cvc
@@ -0,0 +1,15 @@
+% EXPECT: unsat
+% EXIT: 20
+x1, x2: REAL;
+y1, y2: REAL;
+f: REAL -> REAL;
+g: (REAL, REAL) -> REAL;
+
+ASSERT (x1 <= x2) AND (x2 <= x1);
+
+ASSERT NOT (g(x1, y1) = g(x2, y2));
+
+ASSERT (y1 <= f(x1)) AND (f(x1) <= y1);
+ASSERT (y2 <= f(x2)) AND (f(x2) <= y2);
+
+CHECKSAT;
\ No newline at end of file
diff --git a/test/unit/theory/theory_arith_white.h b/test/unit/theory/theory_arith_white.h
index f0073cc0b..4787dfd21 100644
--- a/test/unit/theory/theory_arith_white.h
+++ b/test/unit/theory/theory_arith_white.h
@@ -128,7 +128,7 @@ public:
     Node leq = d_nm->mkNode(LEQ, x, c);
     fakeTheoryEnginePreprocess(leq);
 
-    d_arith->assertFact(leq);
+    d_arith->assertFact(leq, true);
 
     d_arith->check(d_level);
 
@@ -160,7 +160,7 @@ public:
     fakeTheoryEnginePreprocess(leq1);
     fakeTheoryEnginePreprocess(geq1);
 
-    d_arith->assertFact(lt1);
+    d_arith->assertFact(lt1, true);
 
 
     d_arith->check(d_level);
@@ -199,7 +199,7 @@ public:
     fakeTheoryEnginePreprocess(leq1);
     fakeTheoryEnginePreprocess(geq1);
 
-    d_arith->assertFact(leq0);
+    d_arith->assertFact(leq0, true);
 
 
     d_arith->check(d_level);
@@ -235,7 +235,7 @@ public:
     fakeTheoryEnginePreprocess(leq1);
     fakeTheoryEnginePreprocess(geq1);
 
-    d_arith->assertFact(leq1);
+    d_arith->assertFact(leq1, true);
 
 
     d_arith->check(d_level);
diff --git a/test/unit/theory/theory_black.h b/test/unit/theory/theory_black.h
index 63900c19c..be1d4a35b 100644
--- a/test/unit/theory/theory_black.h
+++ b/test/unit/theory/theory_black.h
@@ -214,8 +214,8 @@ public:
   void testDone() {
     TS_ASSERT(d_dummy->doneWrapper());
 
-    d_dummy->assertFact(atom0);
-    d_dummy->assertFact(atom1);
+    d_dummy->assertFact(atom0, true);
+    d_dummy->assertFact(atom1, true);
 
     TS_ASSERT(!d_dummy->doneWrapper());