Fix bug in fmf mbqi=fmc with arrays. Add two datatypes regressions.

diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp
index 3148901da03df232104fcbcdf1f42c93fba8d105..5be26325478c5a718ad615efb5e2198a0fcad336 100644 (file)
--- a/src/theory/quantifiers/full_model_check.cpp
+++ b/src/theory/quantifiers/full_model_check.cpp
@@ -903,6 +903,7 @@ void FullModelChecker::doCheck(FirstOrderModelFmc * fm, Node f, Def & d, Node n
       Trace("fmc-debug") << "Do uninterpreted compose " << n << std::endl;
       //uninterpreted compose
       doUninterpretedCompose( fm, f, d, n.getOperator(), children );
+      /*
     } else if( n.getKind()==SELECT ){
       Trace("fmc-debug") << "Do select compose " << n << std::endl;
       std::vector< Def > children2;
@@ -911,6 +912,7 @@ void FullModelChecker::doCheck(FirstOrderModelFmc * fm, Node f, Def & d, Node n
       mkCondDefaultVec(fm, f, cond);
       std::vector< Node > val;
       doUninterpretedCompose(fm, f, d, children[0], children2, 0, cond, val );
+      */
     } else {
       if( !var_ch.empty() ){
         if( n.getKind()==EQUAL ){

diff --git a/test/regress/regress0/datatypes/Makefile.am b/test/regress/regress0/datatypes/Makefile.am
index b323a27328b7220c1866daf6e7477a9813a75e55..45060dbd33edb90ddd75523cedbeecb0adf12ccc 100644 (file)
--- a/test/regress/regress0/datatypes/Makefile.am
+++ b/test/regress/regress0/datatypes/Makefile.am
@@ -63,7 +63,9 @@ TESTS =       \
        tenum-bug.smt2 \
        cdt-non-canon-stream.smt2 \
        stream-singleton.smt2 \
-       is_test.smt2
+       is_test.smt2 \
+       manos-model.smt2 \
+       bug625.smt2
 
 FAILING_TESTS = \
        datatype-dump.cvc

diff --git a/test/regress/regress0/datatypes/bug625.smt2 b/test/regress/regress0/datatypes/bug625.smt2
new file mode 100644 (file)
index 0000000..3f4312a
--- /dev/null
+++ b/test/regress/regress0/datatypes/bug625.smt2
@@ -0,0 +1,13 @@
+(set-logic ALL_SUPPORTED)
+(set-info :status sat)
+(declare-fun x1 () Int)
+(declare-fun x2 () Int)
+(declare-fun y1 () Int)
+(declare-fun y2 () Int)
+(declare-datatypes () ( (type
+    (constructor1 (f1 Int))
+    (constructor2 (f2 Int))
+)))
+(define-fun mktest ((constructor Int) (p1 Int) (p2 Int)) type (ite (= constructor 1) (constructor1 p1) (constructor2 p2)))
+(assert (distinct (mktest x1 x2 x2) (mktest y1 y2 y2)))
+(check-sat)
\ No newline at end of file

diff --git a/test/regress/regress0/datatypes/manos-model.smt2 b/test/regress/regress0/datatypes/manos-model.smt2
new file mode 100644 (file)
index 0000000..4ade711
--- /dev/null
+++ b/test/regress/regress0/datatypes/manos-model.smt2
@@ -0,0 +1,67 @@
+(set-logic ALL_SUPPORTED)
+(set-info :status unsat)
+(declare-datatypes () ( (tuple2!879 (tuple2!879!880 (_1!881 Int) (_2!882 Int))) ))
+
+(declare-fun p1!207 () tuple2!879)
+
+(declare-fun p2!208 () tuple2!879)
+
+(declare-fun p3!209 () tuple2!879)
+
+(declare-fun reduce!206 (tuple2!879 tuple2!879) tuple2!879)
+
+(assert (not (= 
+    (reduce!206 p1!207 (reduce!206 p2!208 p3!209)) 
+    (reduce!206 (reduce!206 p1!207 p2!208) p3!209)
+)))
+
+(assert (= 
+    (reduce!206 p1!207 (reduce!206 p2!208 p3!209)) 
+    (ite 
+        (>= (_1!881 p1!207) (_2!882 (reduce!206 p2!208 p3!209))) 
+        (tuple2!879!880 
+            (+ (- (_1!881 p1!207) (_2!882 (reduce!206 p2!208 p3!209))) (_1!881 (reduce!206 p2!208 p3!209))) 
+            (_2!882 p1!207)
+        )
+        (tuple2!879!880 
+            (_1!881 (reduce!206 p2!208 p3!209)) 
+            (+ (- (_2!882 (reduce!206 p2!208 p3!209)) (_1!881 p1!207)) (_2!882 p1!207))
+        )
+    )
+))
+
+(assert (= 
+    (reduce!206 p2!208 p3!209) 
+    (ite 
+        (>= (_1!881 p2!208) (_2!882 p3!209))
+        (tuple2!879!880 (+ (- (_1!881 p2!208) (_2!882 p3!209)) (_1!881 p3!209)) (_2!882 p2!208))
+        (tuple2!879!880 (_1!881 p3!209) (+ (- (_2!882 p3!209) (_1!881 p2!208)) (_2!882 p2!208)))
+    )
+))
+
+(assert (= 
+    (reduce!206 (reduce!206 p1!207 p2!208) p3!209) 
+    (ite 
+        (>= (_1!881 (reduce!206 p1!207 p2!208)) (_2!882 p3!209)) 
+        (tuple2!879!880 
+            (+ (- (_1!881 (reduce!206 p1!207 p2!208)) (_2!882 p3!209)) (_1!881 p3!209)) 
+            (_2!882 (reduce!206 p1!207 p2!208))
+        ) 
+        (tuple2!879!880 
+            (_1!881 p3!209) 
+            (+ (- (_2!882 p3!209) (_1!881 (reduce!206 p1!207 p2!208))) (_2!882 (reduce!206 p1!207 p2!208)))
+        )
+    )
+))
+
+(assert (= 
+    (reduce!206 p1!207 p2!208) 
+    (ite 
+        (>= (_1!881 p1!207) (_2!882 p2!208)) 
+        (tuple2!879!880 (+ (- (_1!881 p1!207) (_2!882 p2!208)) (_1!881 p2!208)) (_2!882 p1!207)) 
+        (tuple2!879!880 (_1!881 p2!208) (+ (- (_2!882 p2!208) (_1!881 p1!207)) (_2!882 p1!207)))
+    )
+))
+
+(check-sat)
+