7 files changed, 130 insertions, 3 deletions
diff --git a/test/regress/regress0/datatypes/Makefile.am b/test/regress/regress0/datatypes/Makefile.am
index 45a9d6f30..d06fb1b9b 100644
--- a/test/regress/regress0/datatypes/Makefile.am
+++ b/test/regress/regress0/datatypes/Makefile.am
@@ -67,7 +67,8 @@ TESTS =	\
 	manos-model.smt2 \
 	bug625.smt2 \
 	cdt-model-cade15.smt2 \
-	sc-cdt1.smt2
+	sc-cdt1.smt2  \
+	conqueue-dt-enum-iloop.smt2
 
 FAILING_TESTS = \
 	datatype-dump.cvc
diff --git a/test/regress/regress0/datatypes/conqueue-dt-enum-iloop.smt2 b/test/regress/regress0/datatypes/conqueue-dt-enum-iloop.smt2
new file mode 100644
index 000000000..6f82cd842
--- /dev/null
+++ b/test/regress/regress0/datatypes/conqueue-dt-enum-iloop.smt2
@@ -0,0 +1,75 @@
+(set-logic ALL_SUPPORTED)
+(set-info :status sat)
+(declare-fun start!13 () Bool)
+
+(assert start!13)
+
+(declare-fun b!39 () Bool)
+
+(declare-sort T!14 0)
+
+(declare-datatypes () ( 
+(LazyConQ!5 
+  (Lazyarg1!5 (carry!37 Conc!6) (srear!9 LazyConQ!5)) 
+  (Lazyarg2!5 (t!270 ConQ!6)) 
+  (Lazyarg3!5 (carry!38 Conc!6) (t!271 ConQ!6)) 
+  (Lazyarg4!5 (tree!19 Conc!6) (carry!39 Conc!6)) 
+  (Lazyarg5!5 (tree!20 Conc!6) (carry!40 Conc!6)) 
+  (PushLeft!5 (ys!22 Conc!6) (xs!60 LazyConQ!5)) 
+  (PushLeftLazy!5 (ys!23 Conc!6) (xs!61 LazyConQ!5)))  
+(Conc!6 
+  (CC!5 (left!9 Conc!6) (right!9 Conc!6)) 
+  (Empty!5) 
+  (Single!5 (x!106 T!14)))  
+(ConQ!6 
+  (Spine!5 (head!10 Conc!6) (rear!5 LazyConQ!5)) 
+  (Tip!5 (t!272 Conc!6))) 
+))
+
+(declare-fun e!41 () LazyConQ!5)
+
+(declare-fun l!2 () LazyConQ!5)
+
+(declare-fun st!3 () (Set LazyConQ!5))
+
+(declare-fun firstUnevaluated!3 (LazyConQ!5 (Set LazyConQ!5)) LazyConQ!5)
+
+(declare-fun evalLazyConQ2!7 (LazyConQ!5) ConQ!6)
+
+(assert (=> b!39 (= e!41 (firstUnevaluated!3 (rear!5 (evalLazyConQ2!7 l!2)) st!3))))
+
+(declare-fun b!40 () Bool)
+
+(declare-fun e!42 () LazyConQ!5)
+
+(assert (=> b!40 (= e!42 e!41)))
+
+(assert (=> b!40 (= b!39 (is-Spine!5 (evalLazyConQ2!7 l!2)))))
+
+(declare-fun b!41 () Bool)
+
+(assert (=> b!40 (or (not b!39) (not b!41))))
+
+(assert (=> b!40 (or b!39 b!41)))
+
+(assert (=> b!41 (= e!41 l!2)))
+
+(declare-fun b!42 () Bool)
+
+(assert (=> b!42 (= e!42 l!2)))
+
+(declare-fun lt!14 () LazyConQ!5)
+
+(declare-fun isTip!5 (ConQ!6) Bool)
+
+(assert (=> start!13 (and (not (isTip!5 (evalLazyConQ2!7 lt!14))) (member lt!14 st!3))))
+
+(assert (=> start!13 (= lt!14 e!42)))
+
+(assert (=> start!13 (= b!40 (member l!2 st!3))))
+
+(assert (=> start!13 (or (not b!40) (not b!42))))
+
+(assert (=> start!13 (or b!40 b!42)))
+
+(check-sat)
diff --git a/test/regress/regress0/quantifiers/Makefile.am b/test/regress/regress0/quantifiers/Makefile.am
index e6b0a59fc..939b0d22c 100644
--- a/test/regress/regress0/quantifiers/Makefile.am
+++ b/test/regress/regress0/quantifiers/Makefile.am
@@ -61,7 +61,9 @@ TESTS =	\
 	mix-simp.smt2 \
 	mix-coeff.smt2 \
 	mix-match.smt2 \
-	ari056.smt2
+	ari056.smt2 \
+	ext-ex-deq-trigger.smt2 \
+	matching-lia-1arg.smt2
 
 
 # regression can be solved with --finite-model-find --fmf-inst-engine
diff --git a/test/regress/regress0/quantifiers/ext-ex-deq-trigger.smt2 b/test/regress/regress0/quantifiers/ext-ex-deq-trigger.smt2
new file mode 100644
index 000000000..f6f96fe02
--- /dev/null
+++ b/test/regress/regress0/quantifiers/ext-ex-deq-trigger.smt2
@@ -0,0 +1,26 @@
+; COMMAND-LINE: --relational-triggers
+; EXPECT: unsat
+(set-logic ALL_SUPPORTED)
+(set-info :status unsat)
+
+(declare-sort U 0)
+
+(declare-const k U)
+(declare-const ff U) 
+(declare-const ffk U)
+(declare-fun fun1 (Int) Int)
+(declare-fun fun2 (Int) Int)
+(declare-fun c (U U) U)
+(declare-fun app (U Int) Int)
+
+(assert (forall ((f U) (g U)) (=> (forall ((x Int)) (= (app f x) (app g x))) (= f g))  ))
+
+(assert (forall ((x Int)) (= (app ff x) (+ (fun1 x) (fun2 x)))))
+(assert (forall ((x Int)) (= (app ffk x) (+ (fun1 (app k x)) (fun2 (app k x))))))
+
+(assert (forall ((f U) (g U) (x Int)) (= (app (c f g) x) (app f (app g x)))))
+
+(assert (not (= (c ff k) ffk)))
+
+(check-sat)
+
diff --git a/test/regress/regress0/quantifiers/matching-lia-1arg.smt2 b/test/regress/regress0/quantifiers/matching-lia-1arg.smt2
new file mode 100644
index 000000000..aaf9b2c1f
--- /dev/null
+++ b/test/regress/regress0/quantifiers/matching-lia-1arg.smt2
@@ -0,0 +1,8 @@
+; COMMAND-LINE: --purify-triggers
+; EXPECT: unsat
+(set-logic ALL_SUPPORTED)
+(declare-fun P (Int) Bool)
+(assert (forall ((x Int)) (P (* 2 x))))
+(assert (not (P 38)))
+(check-sat)
+
diff --git a/test/regress/regress0/sygus/Makefile.am b/test/regress/regress0/sygus/Makefile.am
index a1f91a6ce..71ca64aea 100644
--- a/test/regress/regress0/sygus/Makefile.am
+++ b/test/regress/regress0/sygus/Makefile.am
@@ -45,7 +45,8 @@ TESTS = commutative.sy \
         sygus-dt.sy \
         dt-no-syntax.sy \
         list-head-x.sy \
-        clock-inc-tuple.sy
+        clock-inc-tuple.sy \
+        dt-test-ns.sy
 
 # sygus tests currently taking too long for make regress
 EXTRA_DIST = $(TESTS) \
diff --git a/test/regress/regress0/sygus/dt-test-ns.sy b/test/regress/regress0/sygus/dt-test-ns.sy
new file mode 100644
index 000000000..ed17f4ff2
--- /dev/null
+++ b/test/regress/regress0/sygus/dt-test-ns.sy
@@ -0,0 +1,14 @@
+; EXPECT: unsat
+; COMMAND-LINE: --cegqi-si --no-dump-synth
+(set-logic LIA)
+
+(declare-datatypes () ((List (cons (head Int) (tail List)) (nil))))
+
+(synth-fun f ((x Int)) List)
+
+(declare-var x Int)
+
+(constraint (is-cons (f x)))
+(constraint (and (= (head (f x)) x) (= (head (f x)) (+ 5 (head (tail (f x)))))))
+(check-synth)
+