Always split on constructor types for datatypes involving uninterpreted sorts when finite model finding is enabled, add regressions.

4 files changed, 54 insertions, 14 deletions

diff --git a/test/regress/regress0/fmf/Makefile.am b/test/regress/regress0/fmf/Makefile.am
index bb85e62b3..bca9f2e4f 100644
--- a/test/regress/regress0/fmf/Makefile.am
+++ b/test/regress/regress0/fmf/Makefile.am
@@ -41,7 +41,9 @@ TESTS =	\
 	fore19-exp2-core.smt2 \
 	with-ind-104-core.smt2 \
 	syn002-si-real-int.smt2 \
-	krs-sat.smt2
+	krs-sat.smt2 \
+	forall_unit_data2.smt2 \
+	sc_bad_model_1221.smt2
 
 
 EXTRA_DIST = $(TESTS)
diff --git a/test/regress/regress0/fmf/forall_unit_data.smt2 b/test/regress/regress0/fmf/forall_unit_data.smt2
index 7e0897d14..26ef66522 100755
--- a/test/regress/regress0/fmf/forall_unit_data.smt2
+++ b/test/regress/regress0/fmf/forall_unit_data.smt2
@@ -1,13 +1,10 @@
-; cvc4 --lang smt

-

-; This problem returns "unsat", but it is in fact "sat", by interpreting "a" with a domain of

-; cardinality 1. The issue arises irrespective of the "--finite-model-find" option.

-

-(set-option :produce-models true)

-(set-option :interactive-mode true)

-(set-logic ALL_SUPPORTED)

-(declare-sort a 0)

-(declare-datatypes () ((w (Wrap (unw a)))))

-(declare-fun x () w)

-(assert (forall ((y w)) (= x y)))

-(check-sat)

+; COMMAND-LINE: --finite-model-find
+; EXPECT: sat
+(set-option :produce-models true)
+(set-option :interactive-mode true)
+(set-logic ALL_SUPPORTED)
+(declare-sort a 0)
+(declare-datatypes () ((w (Wrap (unw a)))))
+(declare-fun x () w)
+(assert (forall ((y w)) (= x y)))
+(check-sat)
diff --git a/test/regress/regress0/fmf/forall_unit_data2.smt2 b/test/regress/regress0/fmf/forall_unit_data2.smt2
new file mode 100755
index 000000000..64847d6d2
--- /dev/null
+++ b/test/regress/regress0/fmf/forall_unit_data2.smt2
@@ -0,0 +1,8 @@
+; COMMAND-LINE: --finite-model-find
+; EXPECT: unsat
+(set-logic ALL_SUPPORTED)
+(declare-sort a 0)
+(declare-datatypes () ((prod (Pair (gx a) (gy a)))))
+(declare-fun p () prod)
+(assert (forall ((x a) (y a)) (not (= p (Pair x y)))))
+(check-sat)
diff --git a/test/regress/regress0/fmf/sc_bad_model_1221.smt2 b/test/regress/regress0/fmf/sc_bad_model_1221.smt2
new file mode 100755
index 000000000..a083e418d
--- /dev/null
+++ b/test/regress/regress0/fmf/sc_bad_model_1221.smt2
@@ -0,0 +1,33 @@
+; COMMAND-LINE: --finite-model-find
+; EXPECT: sat
+  (set-logic ALL_SUPPORTED)
+  (set-info :status sat)
+  (declare-sort a 0)
+  (declare-fun __nun_card_witness_0 () a)
+  (declare-datatypes () ((prod (Pair (_select_Pair_0 a) (_select_Pair_1 a)))))
+  (declare-sort G_snd 0)
+  (declare-fun __nun_card_witness_1 () G_snd)
+  (declare-fun snd (prod) a)
+  (declare-fun proj_G_snd_0 (G_snd) prod)
+  (assert
+   (forall ((a/32 G_snd))
+      (and
+       (= (snd (proj_G_snd_0 a/32)) (_select_Pair_1 (proj_G_snd_0 a/32))) 
+       true)))
+  (declare-fun p () prod)
+  (declare-datatypes () ((pd (Pd (_select_Pd_0 prod)))))
+  (declare-sort G_fs 0)
+  (declare-fun __nun_card_witness_2 () G_fs)
+  (declare-fun fs (pd) a)
+  (declare-fun proj_G_fs_0 (G_fs) pd)
+  (assert
+   (forall ((a/33 G_fs))
+      (and
+       (= (fs (proj_G_fs_0 a/33))
+        (_select_Pair_0 (_select_Pd_0 (proj_G_fs_0 a/33)))) 
+       true)))
+  (assert
+   (and (not (= (fs (Pd p)) (snd p))) 
+    (exists ((a/34 G_fs)) (= (Pd p) (proj_G_fs_0 a/34))) 
+    (exists ((a/35 G_snd)) (= p (proj_G_snd_0 a/35)))))
+  (check-sat)