added model generation for bv subtheories and bv-inequality solver option

8 files changed, 98 insertions, 0 deletions

diff --git a/test/regress/regress0/datatypes/Makefile.am b/test/regress/regress0/datatypes/Makefile.am
index 08462d51b..8e992c03e 100644
--- a/test/regress/regress0/datatypes/Makefile.am
+++ b/test/regress/regress0/datatypes/Makefile.am
@@ -38,6 +38,12 @@ TESTS =	\
 	typed_v2l30079.cvc \
 	typed_v3l20092.cvc \
 	typed_v5l30069.cvc \
+	boolean-terms-datatype.cvc \
+	boolean-terms-parametric-datatype-1.cvc \
+	boolean-terms-parametric-datatype-2.cvc \
+	boolean-terms-tuple.cvc \
+	boolean-terms-record.cvc \
+	some-boolean-tests.cvc \
 	v10l40099.cvc \
 	v2l40025.cvc \
 	v3l60006.cvc \
@@ -48,6 +54,7 @@ TESTS =	\
 	wrong-sel-simp.cvc
 
 FAILING_TESTS = \
+	pair-real-bool.smt2 \
 	datatype-dump.cvc
 
 EXTRA_DIST = $(TESTS)
diff --git a/test/regress/regress0/datatypes/boolean-terms-datatype.cvc b/test/regress/regress0/datatypes/boolean-terms-datatype.cvc
new file mode 100644
index 000000000..490574b35
--- /dev/null
+++ b/test/regress/regress0/datatypes/boolean-terms-datatype.cvc
@@ -0,0 +1,12 @@
+% EXPECT: sat
+% EXIT: 10
+
+DATATYPE List =
+  cons(car:BOOLEAN, cdr:List) | nil
+END;
+
+x : List;
+
+ASSERT x /= nil;
+
+CHECKSAT;
diff --git a/test/regress/regress0/datatypes/boolean-terms-parametric-datatype-1.cvc b/test/regress/regress0/datatypes/boolean-terms-parametric-datatype-1.cvc
new file mode 100644
index 000000000..b667d0bbc
--- /dev/null
+++ b/test/regress/regress0/datatypes/boolean-terms-parametric-datatype-1.cvc
@@ -0,0 +1,13 @@
+% EXPECT: sat
+% EXIT: 10
+
+DATATYPE RightistTree[T] =
+  node(left:BOOLEAN, right:RightistTree[T]) |
+  leaf(data:T)
+END;
+
+x : RightistTree[INT];
+
+ASSERT x /= leaf(0);
+
+CHECKSAT;
diff --git a/test/regress/regress0/datatypes/boolean-terms-parametric-datatype-2.cvc b/test/regress/regress0/datatypes/boolean-terms-parametric-datatype-2.cvc
new file mode 100644
index 000000000..b667d0bbc
--- /dev/null
+++ b/test/regress/regress0/datatypes/boolean-terms-parametric-datatype-2.cvc
@@ -0,0 +1,13 @@
+% EXPECT: sat
+% EXIT: 10
+
+DATATYPE RightistTree[T] =
+  node(left:BOOLEAN, right:RightistTree[T]) |
+  leaf(data:T)
+END;
+
+x : RightistTree[INT];
+
+ASSERT x /= leaf(0);
+
+CHECKSAT;
diff --git a/test/regress/regress0/datatypes/boolean-terms-record.cvc b/test/regress/regress0/datatypes/boolean-terms-record.cvc
new file mode 100644
index 000000000..ec757d042
--- /dev/null
+++ b/test/regress/regress0/datatypes/boolean-terms-record.cvc
@@ -0,0 +1,8 @@
+% EXPECT: sat
+% EXIT: 10
+
+x : [# i:INT, b:BOOLEAN #];
+
+ASSERT x /= (# i := 0, b := FALSE #);
+
+CHECKSAT;
diff --git a/test/regress/regress0/datatypes/boolean-terms-tuple.cvc b/test/regress/regress0/datatypes/boolean-terms-tuple.cvc
new file mode 100644
index 000000000..c2d95ce8f
--- /dev/null
+++ b/test/regress/regress0/datatypes/boolean-terms-tuple.cvc
@@ -0,0 +1,8 @@
+% EXPECT: sat
+% EXIT: 10
+
+x : [ INT, BOOLEAN ];
+
+ASSERT x /= ( 0, FALSE );
+
+CHECKSAT;
diff --git a/test/regress/regress0/datatypes/pair-real-bool.smt2 b/test/regress/regress0/datatypes/pair-real-bool.smt2
new file mode 100644
index 000000000..5d028d723
--- /dev/null
+++ b/test/regress/regress0/datatypes/pair-real-bool.smt2
@@ -0,0 +1,25 @@
+;(set-option :produce-models true)
+(set-logic QF_ALL_SUPPORTED)
+(set-info :status sat)
+(declare-datatypes () (
+  ( RealTree 
+    ( Node 
+      (left RealTree) 
+		  (elem Real) 
+		  (right RealTree)) 
+    (Leaf)
+   )
+))
+
+(declare-datatypes (T1 T2) ((Pair (mk-pair (first T1) (second T2)))))
+
+( declare-fun SumeAndPositiveTree ( RealTree ) (Pair Real Bool) )
+
+(declare-fun l1 () RealTree)
+(declare-fun l2 () RealTree)
+(declare-const result (Pair Real Bool))
+(assert (= l1 (Node l2 5.0 l2)))
+(assert (= result (SumeAndPositiveTree l1)))
+(assert (= (first result) 5))
+(assert (= (second result) true))
+(check-sat)
diff --git a/test/regress/regress0/datatypes/some-boolean-tests.cvc b/test/regress/regress0/datatypes/some-boolean-tests.cvc
new file mode 100644
index 000000000..ac6ef1137
--- /dev/null
+++ b/test/regress/regress0/datatypes/some-boolean-tests.cvc
@@ -0,0 +1,12 @@
+% EXPECT: sat
+% EXIT: 10
+DATATYPE list[T] = cons(car:T, care:BOOLEAN, cdr:list[T]) | nil END;
+x : list[REAL];
+
+y : [INT,BOOLEAN,INT];
+ASSERT y = (5,TRUE,4);
+
+ASSERT y.1;
+
+ASSERT x = cons(1.1,TRUE,nil::list[REAL])::list[REAL];
+CHECKSAT;