Bug fixes for model construction with codatatypes, add regressions.

5 files changed, 155 insertions, 2 deletions

diff --git a/test/regress/regress0/datatypes/Makefile.am b/test/regress/regress0/datatypes/Makefile.am
index d06fb1b9b..1759d2924 100644
--- a/test/regress/regress0/datatypes/Makefile.am
+++ b/test/regress/regress0/datatypes/Makefile.am
@@ -68,7 +68,8 @@ TESTS =	\
 	bug625.smt2 \
 	cdt-model-cade15.smt2 \
 	sc-cdt1.smt2  \
-	conqueue-dt-enum-iloop.smt2
+	conqueue-dt-enum-iloop.smt2 \
+	coda_simp_model.smt2
 
 FAILING_TESTS = \
 	datatype-dump.cvc
diff --git a/test/regress/regress0/datatypes/coda_simp_model.smt2 b/test/regress/regress0/datatypes/coda_simp_model.smt2
new file mode 100644
index 000000000..1e000cecd
--- /dev/null
+++ b/test/regress/regress0/datatypes/coda_simp_model.smt2
@@ -0,0 +1,12 @@
+(set-logic ALL_SUPPORTED)
+(set-info :status sat)
+(declare-sort a_ 0)
+(declare-fun __nun_card_witness_0 () a_)
+(declare-codatatypes ()
+   ((llist_ (LCons_ (_select_LCons__0 a_) (_select_LCons__1 llist_)) 
+       (LNil_ ))))
+(declare-fun s () llist_)
+(declare-fun a () a_)
+(declare-fun b () a_)
+(assert (= s (LCons_ a (LCons_ b s))))
+(check-sat)
\ No newline at end of file
diff --git a/test/regress/regress0/fmf/Makefile.am b/test/regress/regress0/fmf/Makefile.am
index ff2591a5b..d262d624f 100644
--- a/test/regress/regress0/fmf/Makefile.am
+++ b/test/regress/regress0/fmf/Makefile.am
@@ -45,7 +45,9 @@ TESTS =	\
 	sc_bad_model_1221.smt2 \
  	dt-proper-model.smt2 \
 	fd-false.smt2 \
-	tail_rec.smt2
+	tail_rec.smt2 \
+	jasmin-cdt-crash.smt2 \
+	loopy_coda.smt2
 
 
 EXTRA_DIST = $(TESTS)
diff --git a/test/regress/regress0/fmf/jasmin-cdt-crash.smt2 b/test/regress/regress0/fmf/jasmin-cdt-crash.smt2
new file mode 100644
index 000000000..1f7214232
--- /dev/null
+++ b/test/regress/regress0/fmf/jasmin-cdt-crash.smt2
@@ -0,0 +1,100 @@
+; COMMAND-LINE: --finite-model-find --fmf-inst-engine --uf-ss-fair-monotone
+; EXPECT: sat
+(set-logic ALL_SUPPORTED)
+(set-info :status sat)
+(declare-sort a_ 0)
+(declare-fun __nun_card_witness_0 () a_)
+(declare-codatatypes ()
+   ((llist_ (LCons_ (_select_LCons__0 a_) (_select_LCons__1 llist_)) 
+       (LNil_ ))))
+(declare-fun xs_ () llist_)
+(declare-fun y_ () a_)
+(declare-fun ys_ () llist_)
+(declare-datatypes () ((_nat (_succ (_select__succ_0 _nat)) (_zero ))))
+(declare-fun decr_lprefix_ () _nat)
+(declare-sort G_lprefix__neg 0)
+(declare-fun __nun_card_witness_1 () G_lprefix__neg)
+(declare-fun lprefix__- (_nat llist_ llist_) Bool)
+(declare-fun proj_G_lprefix__neg_0 (G_lprefix__neg) _nat)
+(declare-fun proj_G_lprefix__neg_1 (G_lprefix__neg) llist_)
+(declare-fun proj_G_lprefix__neg_2 (G_lprefix__neg) llist_)
+(assert
+ (forall ((a/60 G_lprefix__neg))
+    (=>
+     (or (= (proj_G_lprefix__neg_0 a/60) _zero) 
+      (and (is-_succ (proj_G_lprefix__neg_0 a/60)) 
+       (= (proj_G_lprefix__neg_1 a/60) LNil_)) 
+      (and
+       (=>
+        (exists ((a/68 G_lprefix__neg))
+           (and
+            (= (_select_LCons__1 (proj_G_lprefix__neg_2 a/60))
+             (proj_G_lprefix__neg_2 a/68)) 
+            (= (_select_LCons__1 (proj_G_lprefix__neg_1 a/60))
+             (proj_G_lprefix__neg_1 a/68)) 
+            (= (_select__succ_0 (proj_G_lprefix__neg_0 a/60))
+             (proj_G_lprefix__neg_0 a/68))))
+        (lprefix__- (_select__succ_0 (proj_G_lprefix__neg_0 a/60)) 
+         (_select_LCons__1 (proj_G_lprefix__neg_1 a/60)) 
+         (_select_LCons__1 (proj_G_lprefix__neg_2 a/60)))) 
+       (is-_succ (proj_G_lprefix__neg_0 a/60)) 
+       (is-LCons_ (proj_G_lprefix__neg_1 a/60)) 
+       (is-LCons_ (proj_G_lprefix__neg_2 a/60)) 
+       (= (_select_LCons__0 (proj_G_lprefix__neg_2 a/60))
+        (_select_LCons__0 (proj_G_lprefix__neg_1 a/60)))))
+     (lprefix__- (proj_G_lprefix__neg_0 a/60) (proj_G_lprefix__neg_1 a/60) 
+      (proj_G_lprefix__neg_2 a/60)))))
+(declare-sort G_lprefix__pos 0)
+(declare-fun __nun_card_witness_2 () G_lprefix__pos)
+(declare-fun lprefix__+ (llist_ llist_) Bool)
+(declare-fun proj_G_lprefix__pos_0 (G_lprefix__pos) llist_)
+(declare-fun proj_G_lprefix__pos_1 (G_lprefix__pos) llist_)
+(assert
+ (forall ((a/69 G_lprefix__pos))
+    (=>
+     (lprefix__+ (proj_G_lprefix__pos_0 a/69) (proj_G_lprefix__pos_1 a/69))
+     (or (= (proj_G_lprefix__pos_0 a/69) LNil_) 
+      (and
+       (lprefix__+ (_select_LCons__1 (proj_G_lprefix__pos_0 a/69)) 
+        (_select_LCons__1 (proj_G_lprefix__pos_1 a/69))) 
+       (exists ((a/77 G_lprefix__pos))
+          (and
+           (= (_select_LCons__1 (proj_G_lprefix__pos_1 a/69))
+            (proj_G_lprefix__pos_1 a/77)) 
+           (= (_select_LCons__1 (proj_G_lprefix__pos_0 a/69))
+            (proj_G_lprefix__pos_0 a/77)))) 
+       (is-LCons_ (proj_G_lprefix__pos_0 a/69)) 
+       (is-LCons_ (proj_G_lprefix__pos_1 a/69)) 
+       (= (_select_LCons__0 (proj_G_lprefix__pos_1 a/69))
+        (_select_LCons__0 (proj_G_lprefix__pos_0 a/69))))))))
+(declare-fun nun_sk_0 () llist_)
+(assert
+ (or
+  (and
+   (not
+    (=>
+     (exists ((a/109 G_lprefix__neg))
+        (and (= (LCons_ y_ ys_) (proj_G_lprefix__neg_2 a/109)) 
+         (= xs_ (proj_G_lprefix__neg_1 a/109)) 
+         (= decr_lprefix_ (proj_G_lprefix__neg_0 a/109))))
+     (lprefix__- decr_lprefix_ xs_ (LCons_ y_ ys_)))) 
+   (or (= xs_ LNil_) 
+    (and (= xs_ (LCons_ y_ nun_sk_0)) (lprefix__+ xs_ ys_) 
+     (exists ((a/113 G_lprefix__pos))
+        (and (= ys_ (proj_G_lprefix__pos_1 a/113)) 
+         (= xs_ (proj_G_lprefix__pos_0 a/113))))))) 
+  (and (not (= xs_ LNil_)) 
+   (forall ((xs_H_/120 llist_))
+      (or (not (= xs_ (LCons_ y_ xs_H_/120))) 
+       (not
+        (=>
+         (exists ((a/124 G_lprefix__neg))
+            (and (= ys_ (proj_G_lprefix__neg_2 a/124)) 
+             (= xs_ (proj_G_lprefix__neg_1 a/124)) 
+             (= decr_lprefix_ (proj_G_lprefix__neg_0 a/124))))
+         (lprefix__- decr_lprefix_ xs_ ys_))))) 
+   (lprefix__+ xs_ (LCons_ y_ ys_)) 
+   (exists ((a/125 G_lprefix__pos))
+      (and (= (LCons_ y_ ys_) (proj_G_lprefix__pos_1 a/125)) 
+       (= xs_ (proj_G_lprefix__pos_0 a/125)))))))
+(check-sat)
diff --git a/test/regress/regress0/fmf/loopy_coda.smt2 b/test/regress/regress0/fmf/loopy_coda.smt2
new file mode 100644
index 000000000..7c1d30886
--- /dev/null
+++ b/test/regress/regress0/fmf/loopy_coda.smt2
@@ -0,0 +1,38 @@
+; COMMAND-LINE: --finite-model-find --fmf-inst-engine --uf-ss-fair-monotone
+; EXPECT: sat
+(set-logic ALL_SUPPORTED)
+(set-info :status sat)
+(declare-sort a 0)
+(declare-fun __nun_card_witness_0 () a)
+(declare-codatatypes ()
+   ((llist (LCons (_select_LCons_0 a) (_select_LCons_1 llist)) (LNil ))))
+(declare-fun xs () llist)
+(declare-fun y () a)
+(declare-fun ys () llist)
+(declare-sort G_lappend 0)
+(declare-fun __nun_card_witness_1 () G_lappend)
+(declare-fun lappend (llist llist) llist)
+(declare-fun proj_G_lappend_0 (G_lappend) llist)
+(declare-fun proj_G_lappend_1 (G_lappend) llist)
+(assert
+ (forall ((a/33 G_lappend))
+    (and
+     (= (lappend (proj_G_lappend_0 a/33) (proj_G_lappend_1 a/33))
+      (ite (is-LCons (proj_G_lappend_0 a/33))
+        (LCons (_select_LCons_0 (proj_G_lappend_0 a/33))
+         (lappend (_select_LCons_1 (proj_G_lappend_0 a/33))
+          (proj_G_lappend_1 a/33)))
+        (proj_G_lappend_1 a/33)))
+     (=> (is-LCons (proj_G_lappend_0 a/33))
+      (exists ((a/35 G_lappend))
+         (and (= (proj_G_lappend_1 a/33) (proj_G_lappend_1 a/35))
+          (= (_select_LCons_1 (proj_G_lappend_0 a/33))
+           (proj_G_lappend_0 a/35))))))))
+(assert
+ (not
+  (=>
+   (exists ((a/37 G_lappend))
+      (and (= (LCons y ys) (proj_G_lappend_1 a/37))
+       (= xs (proj_G_lappend_0 a/37))))
+   (= (lappend xs (LCons y ys)) xs))))
+(check-sat)