update from the master

30 files changed, 661 insertions, 14 deletions

diff --git a/test/regress/regress0/fmf/ForElimination-scala-9.smt2 b/test/regress/regress0/fmf/ForElimination-scala-9.smt2
new file mode 100644
index 000000000..36bb915f4
--- /dev/null
+++ b/test/regress/regress0/fmf/ForElimination-scala-9.smt2
@@ -0,0 +1,31 @@
+; COMMAND-LINE: --finite-model-find --uf-ss=no-minimal
+; EXPECT: unsat
+(set-logic ALL_SUPPORTED)
+(declare-datatypes () ((Statement!1556 (Assign!1557 (varID!1558 (_ BitVec 32)) (expr!1559 Expression!1578)) (Block!1560 (body!1561 List!1617)) (For!1562 (init!1563 Statement!1556) (expr!1564 Expression!1578) (step!1565 Statement!1556) (body!1566 Statement!1556)) (IfThenElse!1567 (expr!1568 Expression!1578) (then!1569 Statement!1556) (elze!1570 Statement!1556)) (Print!1571 (msg!1572 (_ BitVec 32)) (varID!1573 (_ BitVec 32))) (Skip!1574) (While!1575 (expr!1576 Expression!1578) (body!1577 Statement!1556)))
+(Expression!1578 (And!1579 (lhs!1580 Expression!1578) (rhs!1581 Expression!1578)) (Division!1582 (lhs!1583 Expression!1578) (rhs!1584 Expression!1578)) (Equals!1585 (lhs!1586 Expression!1578) (rhs!1587 Expression!1578)) (GreaterThan!1588 (lhs!1589 Expression!1578) (rhs!1590 Expression!1578)) (IntLiteral!1591 (value!1592 (_ BitVec 32))) (LessThan!1593 (lhs!1594 Expression!1578) (rhs!1595 Expression!1578)) (Minus!1596 (lhs!1597 Expression!1578) (rhs!1598 Expression!1578)) (Modulo!1599 (lhs!1600 Expression!1578) (rhs!1601 Expression!1578)) (Neg!1602 (expr!1603 Expression!1578)) (Not!1604 (expr!1605 Expression!1578)) (Or!1606 (lhs!1607 Expression!1578) (rhs!1608 Expression!1578)) (Plus!1609 (lhs!1610 Expression!1578) (rhs!1611 Expression!1578)) (Times!1612 (lhs!1613 Expression!1578) (rhs!1614 Expression!1578)) (Var!1615 (varID!1616 (_ BitVec 32))))
+(List!1617 (Cons!1618 (head!1619 Statement!1556) (tail!1620 List!1617)) (Nil!1621))
+))
+(declare-fun error_value!1622 () Bool)
+(declare-fun ifree (Statement!1556) Bool)
+(declare-fun isForFreeList!223 (List!1617) Bool)
+(declare-fun error_value!1623 () List!1617)
+(declare-fun efll (List!1617) List!1617)
+(declare-fun efl (Statement!1556) Statement!1556)
+(declare-sort I_ifree 0)
+(set-info :notes "ifree_arg_0_1 is op created during fun def fmf")
+(declare-fun ifree_arg_0_1 (I_ifree) Statement!1556)
+(declare-sort I_isForFreeList!223 0)
+(set-info :notes "isForFreeList!223_arg_0_2 is op created during fun def fmf")
+(declare-fun isForFreeList!223_arg_0_2 (I_isForFreeList!223) List!1617)
+(declare-sort I_efll 0)
+(set-info :notes "efll_arg_0_3 is op created during fun def fmf")
+(declare-fun efll_arg_0_3 (I_efll) List!1617)
+(declare-sort I_efl 0)
+(set-info :notes "efl_arg_0_4 is op created during fun def fmf")
+(declare-fun efl_arg_0_4 (I_efl) Statement!1556)
+(assert (forall ((?i I_ifree)) (and (= (ifree (ifree_arg_0_1 ?i)) (ite (is-Block!1560 (ifree_arg_0_1 ?i)) (isForFreeList!223 (body!1561 (ifree_arg_0_1 ?i))) (ite (is-IfThenElse!1567 (ifree_arg_0_1 ?i)) (and (ifree (elze!1570 (ifree_arg_0_1 ?i))) (ifree (then!1569 (ifree_arg_0_1 ?i)))) (ite (is-While!1575 (ifree_arg_0_1 ?i)) (ifree (body!1577 (ifree_arg_0_1 ?i))) (not (is-For!1562 (ifree_arg_0_1 ?i))))))) (ite (is-Block!1560 (ifree_arg_0_1 ?i)) (not (forall ((?z I_isForFreeList!223)) (not (= (isForFreeList!223_arg_0_2 ?z) (body!1561 (ifree_arg_0_1 ?i)))) )) (ite (is-IfThenElse!1567 (ifree_arg_0_1 ?i)) (and (not (forall ((?z I_ifree)) (not (= (ifree_arg_0_1 ?z) (elze!1570 (ifree_arg_0_1 ?i)))) )) (not (forall ((?z I_ifree)) (not (= (ifree_arg_0_1 ?z) (then!1569 (ifree_arg_0_1 ?i)))) ))) (ite (is-While!1575 (ifree_arg_0_1 ?i)) (not (forall ((?z I_ifree)) (not (= (ifree_arg_0_1 ?z) (body!1577 (ifree_arg_0_1 ?i)))) )) true)))) ))
+(assert (forall ((?i I_isForFreeList!223)) (and (= (isForFreeList!223 (isForFreeList!223_arg_0_2 ?i)) (ite (is-Nil!1621 (isForFreeList!223_arg_0_2 ?i)) true (ite (is-Cons!1618 (isForFreeList!223_arg_0_2 ?i)) (and (isForFreeList!223 (tail!1620 (isForFreeList!223_arg_0_2 ?i))) (ifree (head!1619 (isForFreeList!223_arg_0_2 ?i)))) error_value!1622))) (ite (is-Nil!1621 (isForFreeList!223_arg_0_2 ?i)) true (ite (is-Cons!1618 (isForFreeList!223_arg_0_2 ?i)) (and (not (forall ((?z I_isForFreeList!223)) (not (= (isForFreeList!223_arg_0_2 ?z) (tail!1620 (isForFreeList!223_arg_0_2 ?i)))) )) (not (forall ((?z I_ifree)) (not (= (ifree_arg_0_1 ?z) (head!1619 (isForFreeList!223_arg_0_2 ?i)))) ))) true))) ))
+(assert (forall ((?i I_efll)) (and (= (efll (efll_arg_0_3 ?i)) (ite (is-Nil!1621 (efll_arg_0_3 ?i)) Nil!1621 (ite (is-Cons!1618 (efll_arg_0_3 ?i)) (Cons!1618 (efl (head!1619 (efll_arg_0_3 ?i))) (efll (tail!1620 (efll_arg_0_3 ?i)))) error_value!1623))) (ite (is-Nil!1621 (efll_arg_0_3 ?i)) true (ite (is-Cons!1618 (efll_arg_0_3 ?i)) (and (not (forall ((?z I_efl)) (not (= (efl_arg_0_4 ?z) (head!1619 (efll_arg_0_3 ?i)))) )) (not (forall ((?z I_efll)) (not (= (efll_arg_0_3 ?z) (tail!1620 (efll_arg_0_3 ?i)))) ))) true))) ))
+(assert (forall ((?i I_efl)) (and (= (efl (efl_arg_0_4 ?i)) (ite (is-Block!1560 (efl_arg_0_4 ?i)) (Block!1560 (efll (body!1561 (efl_arg_0_4 ?i)))) (ite (is-IfThenElse!1567 (efl_arg_0_4 ?i)) (IfThenElse!1567 (expr!1568 (efl_arg_0_4 ?i)) (efl (then!1569 (efl_arg_0_4 ?i))) (efl (elze!1570 (efl_arg_0_4 ?i)))) (ite (is-While!1575 (efl_arg_0_4 ?i)) (While!1575 (expr!1576 (efl_arg_0_4 ?i)) (efl (body!1577 (efl_arg_0_4 ?i)))) (ite (is-For!1562 (efl_arg_0_4 ?i)) (Block!1560 (Cons!1618 (efl (init!1563 (efl_arg_0_4 ?i))) (Cons!1618 (While!1575 (expr!1564 (efl_arg_0_4 ?i)) (Block!1560 (Cons!1618 (efl (body!1566 (efl_arg_0_4 ?i))) (Cons!1618 (efl (step!1565 (efl_arg_0_4 ?i))) Nil!1621)))) Nil!1621))) (efl_arg_0_4 ?i)))))) (ite (is-Block!1560 (efl_arg_0_4 ?i)) (not (forall ((?z I_efll)) (not (= (efll_arg_0_3 ?z) (body!1561 (efl_arg_0_4 ?i)))) )) (ite (is-IfThenElse!1567 (efl_arg_0_4 ?i)) (and (not (forall ((?z I_efl)) (not (= (efl_arg_0_4 ?z) (then!1569 (efl_arg_0_4 ?i)))) )) (not (forall ((?z I_efl)) (not (= (efl_arg_0_4 ?z) (elze!1570 (efl_arg_0_4 ?i)))) ))) (ite (is-While!1575 (efl_arg_0_4 ?i)) (not (forall ((?z I_efl)) (not (= (efl_arg_0_4 ?z) (body!1577 (efl_arg_0_4 ?i)))) )) (ite (is-For!1562 (efl_arg_0_4 ?i)) (and (not (forall ((?z I_efl)) (not (= (efl_arg_0_4 ?z) (init!1563 (efl_arg_0_4 ?i)))) )) (not (forall ((?z I_efl)) (not (= (efl_arg_0_4 ?z) (body!1566 (efl_arg_0_4 ?i)))) )) (not (forall ((?z I_efl)) (not (= (efl_arg_0_4 ?z) (step!1565 (efl_arg_0_4 ?i)))) ))) true))))) ))
+(assert (exists ((stat!216 Statement!1556)) (not (=> (and (and (and (and (is-For!1562 stat!216) (is-For!1562 stat!216)) (and (ifree (ite (is-Block!1560 (init!1563 stat!216)) (Block!1560 (efll (body!1561 (init!1563 stat!216)))) (ite (is-IfThenElse!1567 (init!1563 stat!216)) (IfThenElse!1567 (expr!1568 (init!1563 stat!216)) (efl (then!1569 (init!1563 stat!216))) (efl (elze!1570 (init!1563 stat!216)))) (ite (is-While!1575 (init!1563 stat!216)) (While!1575 (expr!1576 (init!1563 stat!216)) (efl (body!1577 (init!1563 stat!216)))) (ite (is-For!1562 (init!1563 stat!216)) (Block!1560 (Cons!1618 (efl (init!1563 (init!1563 stat!216))) (Cons!1618 (While!1575 (expr!1564 (init!1563 stat!216)) (Block!1560 (Cons!1618 (efl (body!1566 (init!1563 stat!216))) (Cons!1618 (efl (step!1565 (init!1563 stat!216))) Nil!1621)))) Nil!1621))) (init!1563 stat!216)))))) (not (forall ((?z I_ifree)) (not (= (ifree_arg_0_1 ?z) (ite (is-Block!1560 (init!1563 stat!216)) (Block!1560 (efll (body!1561 (init!1563 stat!216)))) (ite (is-IfThenElse!1567 (init!1563 stat!216)) (IfThenElse!1567 (expr!1568 (init!1563 stat!216)) (efl (then!1569 (init!1563 stat!216))) (efl (elze!1570 (init!1563 stat!216)))) (ite (is-While!1575 (init!1563 stat!216)) (While!1575 (expr!1576 (init!1563 stat!216)) (efl (body!1577 (init!1563 stat!216)))) (ite (is-For!1562 (init!1563 stat!216)) (Block!1560 (Cons!1618 (efl (init!1563 (init!1563 stat!216))) (Cons!1618 (While!1575 (expr!1564 (init!1563 stat!216)) (Block!1560 (Cons!1618 (efl (body!1566 (init!1563 stat!216))) (Cons!1618 (efl (step!1565 (init!1563 stat!216))) Nil!1621)))) Nil!1621))) (init!1563 stat!216))))))) )) (ite (is-Block!1560 (init!1563 stat!216)) (not (forall ((?z I_efll)) (not (= (efll_arg_0_3 ?z) (body!1561 (init!1563 stat!216)))) )) (ite (is-IfThenElse!1567 (init!1563 stat!216)) (and (not (forall ((?z I_efl)) (not (= (efl_arg_0_4 ?z) (then!1569 (init!1563 stat!216)))) )) (not (forall ((?z I_efl)) (not (= (efl_arg_0_4 ?z) (elze!1570 (init!1563 stat!216)))) ))) (ite (is-While!1575 (init!1563 stat!216)) (not (forall ((?z I_efl)) (not (= (efl_arg_0_4 ?z) (body!1577 (init!1563 stat!216)))) )) (ite (is-For!1562 (init!1563 stat!216)) (and (not (forall ((?z I_efl)) (not (= (efl_arg_0_4 ?z) (init!1563 (init!1563 stat!216)))) )) (not (forall ((?z I_efl)) (not (= (efl_arg_0_4 ?z) (body!1566 (init!1563 stat!216)))) )) (not (forall ((?z I_efl)) (not (= (efl_arg_0_4 ?z) (step!1565 (init!1563 stat!216)))) ))) true)))))) (and (ifree (ite (is-Block!1560 (step!1565 stat!216)) (Block!1560 (efll (body!1561 (step!1565 stat!216)))) (ite (is-IfThenElse!1567 (step!1565 stat!216)) (IfThenElse!1567 (expr!1568 (step!1565 stat!216)) (efl (then!1569 (step!1565 stat!216))) (efl (elze!1570 (step!1565 stat!216)))) (ite (is-While!1575 (step!1565 stat!216)) (While!1575 (expr!1576 (step!1565 stat!216)) (efl (body!1577 (step!1565 stat!216)))) (ite (is-For!1562 (step!1565 stat!216)) (Block!1560 (Cons!1618 (efl (init!1563 (step!1565 stat!216))) (Cons!1618 (While!1575 (expr!1564 (step!1565 stat!216)) (Block!1560 (Cons!1618 (efl (body!1566 (step!1565 stat!216))) (Cons!1618 (efl (step!1565 (step!1565 stat!216))) Nil!1621)))) Nil!1621))) (step!1565 stat!216)))))) (not (forall ((?z I_ifree)) (not (= (ifree_arg_0_1 ?z) (ite (is-Block!1560 (step!1565 stat!216)) (Block!1560 (efll (body!1561 (step!1565 stat!216)))) (ite (is-IfThenElse!1567 (step!1565 stat!216)) (IfThenElse!1567 (expr!1568 (step!1565 stat!216)) (efl (then!1569 (step!1565 stat!216))) (efl (elze!1570 (step!1565 stat!216)))) (ite (is-While!1575 (step!1565 stat!216)) (While!1575 (expr!1576 (step!1565 stat!216)) (efl (body!1577 (step!1565 stat!216)))) (ite (is-For!1562 (step!1565 stat!216)) (Block!1560 (Cons!1618 (efl (init!1563 (step!1565 stat!216))) (Cons!1618 (While!1575 (expr!1564 (step!1565 stat!216)) (Block!1560 (Cons!1618 (efl (body!1566 (step!1565 stat!216))) (Cons!1618 (efl (step!1565 (step!1565 stat!216))) Nil!1621)))) Nil!1621))) (step!1565 stat!216))))))) )) (ite (is-Block!1560 (step!1565 stat!216)) (not (forall ((?z I_efll)) (not (= (efll_arg_0_3 ?z) (body!1561 (step!1565 stat!216)))) )) (ite (is-IfThenElse!1567 (step!1565 stat!216)) (and (not (forall ((?z I_efl)) (not (= (efl_arg_0_4 ?z) (then!1569 (step!1565 stat!216)))) )) (not (forall ((?z I_efl)) (not (= (efl_arg_0_4 ?z) (elze!1570 (step!1565 stat!216)))) ))) (ite (is-While!1575 (step!1565 stat!216)) (not (forall ((?z I_efl)) (not (= (efl_arg_0_4 ?z) (body!1577 (step!1565 stat!216)))) )) (ite (is-For!1562 (step!1565 stat!216)) (and (not (forall ((?z I_efl)) (not (= (efl_arg_0_4 ?z) (init!1563 (step!1565 stat!216)))) )) (not (forall ((?z I_efl)) (not (= (efl_arg_0_4 ?z) (body!1566 (step!1565 stat!216)))) )) (not (forall ((?z I_efl)) (not (= (efl_arg_0_4 ?z) (step!1565 (step!1565 stat!216)))) ))) true)))))) (and (ifree (ite (is-Block!1560 (body!1566 stat!216)) (Block!1560 (efll (body!1561 (body!1566 stat!216)))) (ite (is-IfThenElse!1567 (body!1566 stat!216)) (IfThenElse!1567 (expr!1568 (body!1566 stat!216)) (efl (then!1569 (body!1566 stat!216))) (efl (elze!1570 (body!1566 stat!216)))) (ite (is-While!1575 (body!1566 stat!216)) (While!1575 (expr!1576 (body!1566 stat!216)) (efl (body!1577 (body!1566 stat!216)))) (ite (is-For!1562 (body!1566 stat!216)) (Block!1560 (Cons!1618 (efl (init!1563 (body!1566 stat!216))) (Cons!1618 (While!1575 (expr!1564 (body!1566 stat!216)) (Block!1560 (Cons!1618 (efl (body!1566 (body!1566 stat!216))) (Cons!1618 (efl (step!1565 (body!1566 stat!216))) Nil!1621)))) Nil!1621))) (body!1566 stat!216)))))) (not (forall ((?z I_ifree)) (not (= (ifree_arg_0_1 ?z) (ite (is-Block!1560 (body!1566 stat!216)) (Block!1560 (efll (body!1561 (body!1566 stat!216)))) (ite (is-IfThenElse!1567 (body!1566 stat!216)) (IfThenElse!1567 (expr!1568 (body!1566 stat!216)) (efl (then!1569 (body!1566 stat!216))) (efl (elze!1570 (body!1566 stat!216)))) (ite (is-While!1575 (body!1566 stat!216)) (While!1575 (expr!1576 (body!1566 stat!216)) (efl (body!1577 (body!1566 stat!216)))) (ite (is-For!1562 (body!1566 stat!216)) (Block!1560 (Cons!1618 (efl (init!1563 (body!1566 stat!216))) (Cons!1618 (While!1575 (expr!1564 (body!1566 stat!216)) (Block!1560 (Cons!1618 (efl (body!1566 (body!1566 stat!216))) (Cons!1618 (efl (step!1565 (body!1566 stat!216))) Nil!1621)))) Nil!1621))) (body!1566 stat!216))))))) )) (ite (is-Block!1560 (body!1566 stat!216)) (not (forall ((?z I_efll)) (not (= (efll_arg_0_3 ?z) (body!1561 (body!1566 stat!216)))) )) (ite (is-IfThenElse!1567 (body!1566 stat!216)) (and (not (forall ((?z I_efl)) (not (= (efl_arg_0_4 ?z) (then!1569 (body!1566 stat!216)))) )) (not (forall ((?z I_efl)) (not (= (efl_arg_0_4 ?z) (elze!1570 (body!1566 stat!216)))) ))) (ite (is-While!1575 (body!1566 stat!216)) (not (forall ((?z I_efl)) (not (= (efl_arg_0_4 ?z) (body!1577 (body!1566 stat!216)))) )) (ite (is-For!1562 (body!1566 stat!216)) (and (not (forall ((?z I_efl)) (not (= (efl_arg_0_4 ?z) (init!1563 (body!1566 stat!216)))) )) (not (forall ((?z I_efl)) (not (= (efl_arg_0_4 ?z) (body!1566 (body!1566 stat!216)))) )) (not (forall ((?z I_efl)) (not (= (efl_arg_0_4 ?z) (step!1565 (body!1566 stat!216)))) ))) true)))))) (or (ifree (ite (is-Block!1560 stat!216) (Block!1560 (efll (body!1561 stat!216))) (ite (is-IfThenElse!1567 stat!216) (IfThenElse!1567 (expr!1568 stat!216) (efl (then!1569 stat!216)) (efl (elze!1570 stat!216))) (ite (is-While!1575 stat!216) (While!1575 (expr!1576 stat!216) (efl (body!1577 stat!216))) (ite (is-For!1562 stat!216) (Block!1560 (Cons!1618 (efl (init!1563 stat!216)) (Cons!1618 (While!1575 (expr!1564 stat!216) (Block!1560 (Cons!1618 (efl (body!1566 stat!216)) (Cons!1618 (efl (step!1565 stat!216)) Nil!1621)))) Nil!1621))) stat!216))))) (forall ((?z I_ifree)) (not (= (ifree_arg_0_1 ?z) (ite (is-Block!1560 stat!216) (Block!1560 (efll (body!1561 stat!216))) (ite (is-IfThenElse!1567 stat!216) (IfThenElse!1567 (expr!1568 stat!216) (efl (then!1569 stat!216)) (efl (elze!1570 stat!216))) (ite (is-While!1575 stat!216) (While!1575 (expr!1576 stat!216) (efl (body!1577 stat!216))) (ite (is-For!1562 stat!216) (Block!1560 (Cons!1618 (efl (init!1563 stat!216)) (Cons!1618 (While!1575 (expr!1564 stat!216) (Block!1560 (Cons!1618 (efl (body!1566 stat!216)) (Cons!1618 (efl (step!1565 stat!216)) Nil!1621)))) Nil!1621))) stat!216)))))) ) (not (ite (is-Block!1560 stat!216) (not (forall ((?z I_efll)) (not (= (efll_arg_0_3 ?z) (body!1561 stat!216))) )) (ite (is-IfThenElse!1567 stat!216) (and (not (forall ((?z I_efl)) (not (= (efl_arg_0_4 ?z) (then!1569 stat!216))) )) (not (forall ((?z I_efl)) (not (= (efl_arg_0_4 ?z) (elze!1570 stat!216))) ))) (ite (is-While!1575 stat!216) (not (forall ((?z I_efl)) (not (= (efl_arg_0_4 ?z) (body!1577 stat!216))) )) (ite (is-For!1562 stat!216) (and (not (forall ((?z I_efl)) (not (= (efl_arg_0_4 ?z) (init!1563 stat!216))) )) (not (forall ((?z I_efl)) (not (= (efl_arg_0_4 ?z) (body!1566 stat!216))) )) (not (forall ((?z I_efl)) (not (= (efl_arg_0_4 ?z) (step!1565 stat!216))) ))) true)))))))) ))
+(check-sat)
diff --git a/test/regress/regress0/fmf/LeftistHeap.scala-8-ncm.smt2 b/test/regress/regress0/fmf/LeftistHeap.scala-8-ncm.smt2
new file mode 100644
index 000000000..9ef5f14fa
--- /dev/null
+++ b/test/regress/regress0/fmf/LeftistHeap.scala-8-ncm.smt2
@@ -0,0 +1,33 @@
+; COMMAND-LINE: --finite-model-find
+; EXPECT: sat
+(set-logic ALL_SUPPORTED)
+(set-info :status sat)
+(declare-datatypes () ((array!896 (array!896!897 (size!898 (_ BitVec 32)) (content!899 (Array (_ BitVec 32) (_ BitVec 32)))))))
+(declare-datatypes () ((tuple2!900 (tuple2!900!901 (_1!902 array!896) (_2!903 (_ BitVec 32))))))
+(declare-fun error_value!904 () (_ BitVec 32))
+(declare-fun error_value!905 () (_ BitVec 32))
+(declare-fun error_value!906 () array!896)
+(declare-fun error_value!907 () (_ BitVec 32))
+(declare-fun error_value!908 () array!896)
+(declare-fun error_value!909 () (_ BitVec 32))
+(declare-fun while0!216 (array!896 (_ BitVec 32) array!896) tuple2!900)
+(declare-fun isPositive!206 (array!896 (_ BitVec 32)) Bool)
+(declare-fun rec!210 ((_ BitVec 32) array!896 (_ BitVec 32)) Bool)
+(declare-fun arrayconst!910 () (Array (_ BitVec 32) (_ BitVec 32)))
+(declare-sort I_while0!216 0)
+(declare-fun while0!216_arg_0_1 (I_while0!216) array!896)
+(declare-fun while0!216_arg_1_2 (I_while0!216) (_ BitVec 32))
+(declare-fun while0!216_arg_2_3 (I_while0!216) array!896)
+(declare-sort I_isPositive!206 0)
+(declare-fun isPositive!206_arg_0_4 (I_isPositive!206) array!896)
+(declare-fun isPositive!206_arg_1_5 (I_isPositive!206) (_ BitVec 32))
+(declare-sort I_rec!210 0)
+(declare-fun rec!210_arg_0_6 (I_rec!210) (_ BitVec 32))
+(declare-fun rec!210_arg_1_7 (I_rec!210) array!896)
+(declare-fun rec!210_arg_2_8 (I_rec!210) (_ BitVec 32))
+(assert (forall ((?i I_while0!216)) (and (= (while0!216 (while0!216_arg_0_1 ?i) (while0!216_arg_1_2 ?i) (while0!216_arg_2_3 ?i)) (ite (bvslt (while0!216_arg_1_2 ?i) (size!898 (while0!216_arg_2_3 ?i))) (while0!216 (ite (bvslt (ite (and (bvslt (while0!216_arg_1_2 ?i) (size!898 (while0!216_arg_2_3 ?i))) (not (bvslt (while0!216_arg_1_2 ?i) (_ bv0 32)))) (select (content!899 (while0!216_arg_2_3 ?i)) (while0!216_arg_1_2 ?i)) error_value!904) (_ bv0 32)) (ite (and (bvslt (while0!216_arg_1_2 ?i) (size!898 (while0!216_arg_0_1 ?i))) (not (bvslt (while0!216_arg_1_2 ?i) (_ bv0 32)))) (array!896!897 (size!898 (while0!216_arg_0_1 ?i)) (store (content!899 (while0!216_arg_0_1 ?i)) (while0!216_arg_1_2 ?i) (bvneg (ite (and (bvslt (while0!216_arg_1_2 ?i) (size!898 (while0!216_arg_2_3 ?i))) (not (bvslt (while0!216_arg_1_2 ?i) (_ bv0 32)))) (select (content!899 (while0!216_arg_2_3 ?i)) (while0!216_arg_1_2 ?i)) error_value!905)))) error_value!906) (ite (and (bvslt (while0!216_arg_1_2 ?i) (size!898 (while0!216_arg_0_1 ?i))) (not (bvslt (while0!216_arg_1_2 ?i) (_ bv0 32)))) (array!896!897 (size!898 (while0!216_arg_0_1 ?i)) (store (content!899 (while0!216_arg_0_1 ?i)) (while0!216_arg_1_2 ?i) (ite (and (bvslt (while0!216_arg_1_2 ?i) (size!898 (while0!216_arg_2_3 ?i))) (not (bvslt (while0!216_arg_1_2 ?i) (_ bv0 32)))) (select (content!899 (while0!216_arg_2_3 ?i)) (while0!216_arg_1_2 ?i)) error_value!907))) error_value!908)) (bvadd (while0!216_arg_1_2 ?i) (_ bv1 32)) (while0!216_arg_2_3 ?i)) (tuple2!900!901 (while0!216_arg_0_1 ?i) (while0!216_arg_1_2 ?i)))) (ite (bvslt (while0!216_arg_1_2 ?i) (size!898 (while0!216_arg_2_3 ?i))) (not (forall ((?z I_while0!216)) (not (and (= (while0!216_arg_0_1 ?z) (ite (bvslt (ite (and (bvslt (while0!216_arg_1_2 ?i) (size!898 (while0!216_arg_2_3 ?i))) (not (bvslt (while0!216_arg_1_2 ?i) (_ bv0 32)))) (select (content!899 (while0!216_arg_2_3 ?i)) (while0!216_arg_1_2 ?i)) error_value!904) (_ bv0 32)) (ite (and (bvslt (while0!216_arg_1_2 ?i) (size!898 (while0!216_arg_0_1 ?i))) (not (bvslt (while0!216_arg_1_2 ?i) (_ bv0 32)))) (array!896!897 (size!898 (while0!216_arg_0_1 ?i)) (store (content!899 (while0!216_arg_0_1 ?i)) (while0!216_arg_1_2 ?i) (bvneg (ite (and (bvslt (while0!216_arg_1_2 ?i) (size!898 (while0!216_arg_2_3 ?i))) (not (bvslt (while0!216_arg_1_2 ?i) (_ bv0 32)))) (select (content!899 (while0!216_arg_2_3 ?i)) (while0!216_arg_1_2 ?i)) error_value!905)))) error_value!906) (ite (and (bvslt (while0!216_arg_1_2 ?i) (size!898 (while0!216_arg_0_1 ?i))) (not (bvslt (while0!216_arg_1_2 ?i) (_ bv0 32)))) (array!896!897 (size!898 (while0!216_arg_0_1 ?i)) (store (content!899 (while0!216_arg_0_1 ?i)) (while0!216_arg_1_2 ?i) (ite (and (bvslt (while0!216_arg_1_2 ?i) (size!898 (while0!216_arg_2_3 ?i))) (not (bvslt (while0!216_arg_1_2 ?i) (_ bv0 32)))) (select (content!899 (while0!216_arg_2_3 ?i)) (while0!216_arg_1_2 ?i)) error_value!907))) error_value!908))) (= (while0!216_arg_1_2 ?z) (bvadd (while0!216_arg_1_2 ?i) (_ bv1 32))) (= (while0!216_arg_2_3 ?z) (while0!216_arg_2_3 ?i)))) )) true)) ))
+(assert (forall ((?i I_isPositive!206)) (and (= (isPositive!206 (isPositive!206_arg_0_4 ?i) (isPositive!206_arg_1_5 ?i)) (rec!210 (_ bv0 32) (isPositive!206_arg_0_4 ?i) (isPositive!206_arg_1_5 ?i))) (not (forall ((?z I_rec!210)) (not (and (= (rec!210_arg_0_6 ?z) (_ bv0 32)) (= (rec!210_arg_1_7 ?z) (isPositive!206_arg_0_4 ?i)) (= (rec!210_arg_2_8 ?z) (isPositive!206_arg_1_5 ?i)))) ))) ))
+(assert (forall ((?i I_rec!210)) (and (= (rec!210 (rec!210_arg_0_6 ?i) (rec!210_arg_1_7 ?i) (rec!210_arg_2_8 ?i)) (ite (not (bvslt (rec!210_arg_0_6 ?i) (rec!210_arg_2_8 ?i))) true (ite (bvslt (ite (and (bvslt (rec!210_arg_0_6 ?i) (size!898 (rec!210_arg_1_7 ?i))) (not (bvslt (rec!210_arg_0_6 ?i) (_ bv0 32)))) (select (content!899 (rec!210_arg_1_7 ?i)) (rec!210_arg_0_6 ?i)) error_value!909) (_ bv0 32)) false (rec!210 (bvadd (rec!210_arg_0_6 ?i) (_ bv1 32)) (rec!210_arg_1_7 ?i) (rec!210_arg_2_8 ?i))))) (ite (not (bvslt (rec!210_arg_0_6 ?i) (rec!210_arg_2_8 ?i))) true (ite (bvslt (ite (and (bvslt (rec!210_arg_0_6 ?i) (size!898 (rec!210_arg_1_7 ?i))) (not (bvslt (rec!210_arg_0_6 ?i) (_ bv0 32)))) (select (content!899 (rec!210_arg_1_7 ?i)) (rec!210_arg_0_6 ?i)) error_value!909) (_ bv0 32)) true (not (forall ((?z I_rec!210)) (not (and (= (rec!210_arg_0_6 ?z) (bvadd (rec!210_arg_0_6 ?i) (_ bv1 32))) (= (rec!210_arg_1_7 ?z) (rec!210_arg_1_7 ?i)) (= (rec!210_arg_2_8 ?z) (rec!210_arg_2_8 ?i)))) ))))) ))
+(assert (not (forall ((tab!211 array!896)) (or (or (bvslt (size!898 (_1!902 (while0!216 (array!896!897 (size!898 tab!211) arrayconst!910) (_ bv0 32) tab!211))) (_ bv0 32)) (forall ((?z I_while0!216)) (not (and (= (while0!216_arg_0_1 ?z) (array!896!897 (size!898 tab!211) arrayconst!910)) (= (while0!216_arg_1_2 ?z) (_ bv0 32)) (= (while0!216_arg_2_3 ?z) tab!211))) )) (or (isPositive!206 (_1!902 (while0!216 (array!896!897 (size!898 tab!211) arrayconst!910) (_ bv0 32) tab!211)) (size!898 tab!211)) (forall ((?z I_isPositive!206)) (not (and (= (isPositive!206_arg_0_4 ?z) (_1!902 (while0!216 (array!896!897 (size!898 tab!211) arrayconst!910) (_ bv0 32) tab!211))) (= (isPositive!206_arg_1_5 ?z) (size!898 tab!211)))) ) (forall ((?z I_while0!216)) (not (and (= (while0!216_arg_0_1 ?z) (array!896!897 (size!898 tab!211) arrayconst!910)) (= (while0!216_arg_1_2 ?z) (_ bv0 32)) (= (while0!216_arg_2_3 ?z) tab!211))) ))) )))
+(check-sat)
+
diff --git a/test/regress/regress0/fmf/Makefile.am b/test/regress/regress0/fmf/Makefile.am
index 8cff980a5..575aa4159 100644
--- a/test/regress/regress0/fmf/Makefile.am
+++ b/test/regress/regress0/fmf/Makefile.am
@@ -50,8 +50,12 @@ TESTS =	\
 	loopy_coda.smt2 \
 	fmc_unsound_model.smt2 \
 	am-bad-model.cvc \
-	nun-0208-to.smt2
-
+	nun-0208-to.smt2 \
+	datatypes-ufinite.smt2 \
+	datatypes-ufinite-nested.smt2 \
+	ForElimination-scala-9.smt2 \
+	agree466.smt2 \
+	LeftistHeap.scala-8-ncm.smt2
 
 EXTRA_DIST = $(TESTS)
 
@@ -66,7 +70,6 @@ EXTRA_DIST = $(TESTS)
 #EXTRA_DIST += \
 #	error.cvc
 
-# agree466.smt2 timeout after commit on 1/14 due to Array+FMF model construction
 
 # synonyms for "check" in this directory
 .PHONY: regress regress0 test
diff --git a/test/regress/regress0/fmf/datatypes-ufinite-nested.smt2 b/test/regress/regress0/fmf/datatypes-ufinite-nested.smt2
new file mode 100644
index 000000000..3ffc36d05
--- /dev/null
+++ b/test/regress/regress0/fmf/datatypes-ufinite-nested.smt2
@@ -0,0 +1,17 @@
+; COMMAND-LINE: --finite-model-find
+; EXPECT: sat
+(set-logic ALL_SUPPORTED)
+(declare-sort U 0)
+(declare-fun a () U)
+(declare-fun b () U)
+(declare-fun c () U)
+(declare-fun d () U)
+(assert (distinct a b c))
+(declare-sort V 0)
+(declare-datatypes () ((ufin1 (cons1 (s11 U) (s13 ufin2))) (ufin2 (cons2 (s21 V) (s22 U)) (cons3))))
+(declare-fun P (ufin1 ufin2) Bool)
+(declare-fun Q (ufin1 ufin1) Bool)
+(assert (forall ((x ufin1) (y ufin2) (z ufin1)) (or (P x y) (Q x z))))
+(assert (not (P (cons1 a cons3) cons3)))
+(assert (not (Q (cons1 b cons3) (cons1 a cons3))))
+(check-sat)
diff --git a/test/regress/regress0/fmf/datatypes-ufinite.smt2 b/test/regress/regress0/fmf/datatypes-ufinite.smt2
new file mode 100644
index 000000000..3564bff8b
--- /dev/null
+++ b/test/regress/regress0/fmf/datatypes-ufinite.smt2
@@ -0,0 +1,17 @@
+; COMMAND-LINE: --finite-model-find
+; EXPECT: sat
+(set-logic ALL_SUPPORTED)
+(declare-sort U 0)
+(declare-fun a () U)
+(declare-fun b () U)
+(declare-fun c () U)
+(declare-fun d () U)
+(assert (distinct a b c))
+(declare-sort V 0)
+(declare-datatypes () ((ufin1 (cons1 (s11 U) (s12 U))) (ufin2 (cons2 (s21 V) (s22 U)) (cons3))))
+(declare-fun P (ufin1 ufin2) Bool)
+(declare-fun Q (ufin1 ufin1) Bool)
+(assert (forall ((x ufin1) (y ufin2) (z ufin1)) (or (P x y) (Q x z))))
+(assert (not (P (cons1 a a) cons3)))
+(assert (not (Q (cons1 a d) (cons1 a b))))
+(check-sat)
diff --git a/test/regress/regress0/push-pop/Makefile.am b/test/regress/regress0/push-pop/Makefile.am
index bcf6403b7..4bc16ea25 100644
--- a/test/regress/regress0/push-pop/Makefile.am
+++ b/test/regress/regress0/push-pop/Makefile.am
@@ -44,7 +44,8 @@ BUG_TESTS = \
   bug-fmf-fun-skolem.smt2 \
   bug674.smt2 \
   inc-double-u.smt2 \
-  fmf-fun-dbu.smt2
+  fmf-fun-dbu.smt2 \
+  inc-define.smt2
 
 TESTS =	$(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(BUG_TESTS)
 
diff --git a/test/regress/regress0/push-pop/inc-define.smt2 b/test/regress/regress0/push-pop/inc-define.smt2
new file mode 100644
index 000000000..27261eff6
--- /dev/null
+++ b/test/regress/regress0/push-pop/inc-define.smt2
@@ -0,0 +1,9 @@
+; COMMAND-LINE: --incremental
+; EXPECT: sat
+; EXPECT: sat
+(set-logic QF_LIA)
+(declare-fun x () Int)
+(check-sat)
+(define t (not (= x 0)))
+(assert t)
+(check-sat)
diff --git a/test/regress/regress0/quantifiers/Makefile.am b/test/regress/regress0/quantifiers/Makefile.am
index df146752e..6b5e0d1ed 100644
--- a/test/regress/regress0/quantifiers/Makefile.am
+++ b/test/regress/regress0/quantifiers/Makefile.am
@@ -38,10 +38,9 @@ TESTS =	\
 	gauss_init_0030.fof.smt2 \
 	qcft-javafe.filespace.TreeWalker.006.smt2 \
 	qcft-smtlib3dbc51.smt2 \
-	symmetric_unsat_7.smt2 \
 	javafe.ast.StmtVec.009.smt2 \
 	ARI176e1.smt2 \
-  bi-artm-s.smt2 \
+	bi-artm-s.smt2 \
 	simp-typ-test.smt2 \
 	macros-int-real.smt2 \
 	stream-x2014-09-18-unsat.smt2 \
@@ -65,12 +64,22 @@ TESTS =	\
 	ext-ex-deq-trigger.smt2 \
 	matching-lia-1arg.smt2 \
 	RND_4_16.smt2 \
-  cdt-0208-to.smt2 \
-  psyco-196.smt2 \
-  agg-rew-test.smt2 \
-  agg-rew-test-cf.smt2 \
-  rew-to-0211-dd.smt2 \
-  rew-to-scala.smt2
+	cdt-0208-to.smt2 \
+	psyco-196.smt2 \
+	agg-rew-test.smt2 \
+	agg-rew-test-cf.smt2 \
+	rew-to-0211-dd.smt2 \
+	rew-to-scala.smt2 \
+	macro-subtype-param.smt2 \
+	macros-real-arg.smt2 \
+	subtype-param-unk.smt2 \
+	subtype-param.smt2 \
+	anti-sk-simp.smt2 \
+	pure_dt_cbqi.smt2 \
+	florian-case-ax.smt2 \
+	double-pattern.smt2 \
+	qcf-rel-dom-opt.smt2 \
+	parametric-lists.smt2
 
 
 # regression can be solved with --finite-model-find --fmf-inst-engine
diff --git a/test/regress/regress0/quantifiers/anti-sk-simp.smt2 b/test/regress/regress0/quantifiers/anti-sk-simp.smt2
new file mode 100755
index 000000000..ba4f9cbb9
--- /dev/null
+++ b/test/regress/regress0/quantifiers/anti-sk-simp.smt2
@@ -0,0 +1,10 @@
+; COMMAND-LINE: --quant-anti-skolem
+; EXPECT: unsat
+(set-logic ALL_SUPPORTED)
+(set-info :status unsat)
+(declare-fun f (Int) Int)
+(declare-fun a () Int)
+(declare-fun b () Int)
+(assert (forall ((X Int)) (< X (f X))))
+(assert (forall ((X Int)) (> (+ a b) (f X))))
+(check-sat)
diff --git a/test/regress/regress0/quantifiers/double-pattern.smt2 b/test/regress/regress0/quantifiers/double-pattern.smt2
new file mode 100644
index 000000000..4ce21d446
--- /dev/null
+++ b/test/regress/regress0/quantifiers/double-pattern.smt2
@@ -0,0 +1,6 @@
+(set-logic UFLIA)
+(set-info :status unsat)
+(declare-fun P (Int) Bool)
+(assert (forall ((x Int)) (! (! (P x) :pattern ((P x))) :pattern ((P x)))))
+(assert (not (P 0)))
+(check-sat)
diff --git a/test/regress/regress0/quantifiers/florian-case-ax.smt2 b/test/regress/regress0/quantifiers/florian-case-ax.smt2
new file mode 100644
index 000000000..35ebb28e9
--- /dev/null
+++ b/test/regress/regress0/quantifiers/florian-case-ax.smt2
@@ -0,0 +1,168 @@
+(set-logic AUFLIA)
+(set-info :status unsat)
+(declare-sort U 0)
+(declare-fun A (U U U
+  U U U U
+  U U U U
+  U U U U
+  U U U U
+  U U U U
+  U U U U
+  U U U U
+  U U U U
+  U U U U
+  U U U U
+  U U U U
+  U U U U
+  U U U U
+  U U
+  U) (Array Int U))
+
+(assert
+  (forall ((v_184 U) (v_185 U)
+  (v_186 U) (v_187 U)
+  (v_188 U) (v_189 U)
+  (v_190 U) (v_191 U)
+  (v_192 U) (v_193 U)
+  (v_194 U) (v_195 U)
+  (v_196 U) (v_197 U)
+  (v_198 U) (v_199 U)
+  (v_200 U) (v_201 U)
+  (v_202 U) (v_203 U)
+  (v_204 U) (v_205 U)
+  (v_206 U) (v_207 U)
+  (v_208 U) (v_209 U)
+  (v_210 U) (v_211 U)
+  (v_212 U) (v_213 U)
+  (v_214 U) (v_215 U)
+  (v_216 U) (v_217 U)
+  (v_218 U) (v_219 U)
+  (v_220 U) (v_221 U)
+  (v_222 U) (v_223 U)
+  (v_224 U) (v_225 U)
+  (v_226 U) (v_227 U)
+  (v_228 U) (v_229 U)
+  (v_230 U) (v_231 U)
+  (v_232 U) (v_233 U)
+  (v_234 U) (v_235 U)
+  (v_236 U) (v_237 U)
+  (v_238 U) (v_239 U)
+  (v_240 U) (v_241 U) (v_242 Int))
+  (let ((v_183 (A v_184 v_185 v_186 v_187
+                    v_188 v_189 v_190 v_191 v_192
+                    v_193 v_194 v_195 v_196 v_197
+                    v_198 v_199 v_200 v_201 v_202
+                    v_203 v_204 v_205 v_206 v_207
+                    v_208 v_209 v_210 v_211 v_212
+                    v_213 v_214 v_215 v_216 v_217
+                    v_218 v_219 v_220 v_221 v_222
+                    v_223 v_224 v_225 v_226 v_227
+                    v_228 v_229 v_230 v_231 v_232
+                    v_233 v_234 v_235 v_236 v_237
+                    v_238 v_239 v_240 v_241)))
+  (ite (= v_242 59) (= (select v_183 v_242) v_240)
+  (ite (= v_242 58) (= (select v_183 v_242) v_239)
+  (ite (= v_242 57) (= (select v_183 v_242) v_238)
+  (ite (= v_242 56) (= (select v_183 v_242) v_237)
+  (ite (= v_242 55) (= (select v_183 v_242) v_236)
+  (ite (= v_242 54) (= (select v_183 v_242) v_235)
+  (ite (= v_242 53) (= (select v_183 v_242) v_234)
+  (ite (= v_242 52) (= (select v_183 v_242) v_233)
+  (ite (= v_242 51) (= (select v_183 v_242) v_232)
+  (ite (= v_242 50) (= (select v_183 v_242) v_231)
+  (ite (= v_242 49) (= (select v_183 v_242) v_230)
+  (ite (= v_242 48) (= (select v_183 v_242) v_229)
+  (ite (= v_242 47) (= (select v_183 v_242) v_228)
+  (ite (= v_242 46) (= (select v_183 v_242) v_227)
+  (ite (= v_242 45) (= (select v_183 v_242) v_226)
+  (ite (= v_242 44) (= (select v_183 v_242) v_225)
+  (ite (= v_242 43) (= (select v_183 v_242) v_224)
+  (ite (= v_242 41) (= (select v_183 v_242) v_223)
+  (ite (= v_242 40) (= (select v_183 v_242) v_222)
+  (ite (= v_242 39) (= (select v_183 v_242) v_221)
+  (ite (= v_242 37) (= (select v_183 v_242) v_220)
+  (ite (= v_242 36) (= (select v_183 v_242) v_219)
+  (ite (= v_242 34) (= (select v_183 v_242) v_218)
+  (ite (= v_242 33) (= (select v_183 v_242) v_217)
+  (ite (= v_242 32) (= (select v_183 v_242) v_216)
+  (ite (= v_242 31) (= (select v_183 v_242) v_215)
+  (ite (= v_242 30) (= (select v_183 v_242) v_214)
+  (ite (= v_242 29) (= (select v_183 v_242) v_213)
+  (ite (= v_242 28) (= (select v_183 v_242) v_212)
+  (ite (= v_242 27) (= (select v_183 v_242) v_211)
+  (ite (= v_242 26) (= (select v_183 v_242) v_210)
+  (ite (= v_242 25) (= (select v_183 v_242) v_209)
+  (ite (= v_242 24) (= (select v_183 v_242) v_208)
+  (ite (= v_242 23) (= (select v_183 v_242) v_207)
+  (ite (= v_242 22) (= (select v_183 v_242) v_206)
+  (ite (= v_242 21) (= (select v_183 v_242) v_205)
+  (ite (= v_242 20) (= (select v_183 v_242) v_204)
+  (ite (= v_242 19) (= (select v_183 v_242) v_203)
+  (ite (= v_242 18) (= (select v_183 v_242) v_202)
+  (ite (= v_242 17) (= (select v_183 v_242) v_201)
+  (ite (= v_242 16) (= (select v_183 v_242) v_200)
+  (ite (= v_242 15) (= (select v_183 v_242) v_199)
+  (ite (= v_242 14) (= (select v_183 v_242) v_198)
+  (ite (= v_242 13) (= (select v_183 v_242) v_197)
+  (ite (= v_242 12) (= (select v_183 v_242) v_196)
+  (ite (= v_242 11) (= (select v_183 v_242) v_195)
+  (ite (= v_242 10) (= (select v_183 v_242) v_194)
+  (ite (= v_242 9) (= (select v_183 v_242) v_193)
+  (ite (= v_242 8) (= (select v_183 v_242) v_192)
+  (ite (= v_242 7) (= (select v_183 v_242) v_191)
+  (ite (= v_242 6) (= (select v_183 v_242) v_190)
+  (ite (= v_242 5) (= (select v_183 v_242) v_189)
+  (ite (= v_242 4) (= (select v_183 v_242) v_188)
+  (ite (= v_242 3) (= (select v_183 v_242) v_187)
+  (ite (= v_242 2) (= (select v_183 v_242) v_186)
+  (ite (= v_242 1) (= (select v_183 v_242) v_185)
+  (ite (= v_242 0) (= (select v_183 v_242) v_184)
+  (= (select v_183 v_242) v_241)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
+  
+(declare-const c_184 U) (declare-const c_185 U)
+(declare-const c_186 U) (declare-const c_187 U)
+(declare-const c_188 U) (declare-const c_189 U)
+(declare-const c_190 U) (declare-const c_191 U)
+(declare-const c_192 U) (declare-const c_193 U)
+(declare-const c_194 U) (declare-const c_195 U)
+(declare-const c_196 U) (declare-const c_197 U)
+(declare-const c_198 U) (declare-const c_199 U)
+(declare-const c_200 U) (declare-const c_201 U)
+(declare-const c_202 U) (declare-const c_203 U)
+(declare-const c_204 U) (declare-const c_205 U)
+(declare-const c_206 U) (declare-const c_207 U)
+(declare-const c_208 U) (declare-const c_209 U)
+(declare-const c_210 U) (declare-const c_211 U)
+(declare-const c_212 U) (declare-const c_213 U)
+(declare-const c_214 U) (declare-const c_215 U)
+(declare-const c_216 U) (declare-const c_217 U)
+(declare-const c_218 U) (declare-const c_219 U)
+(declare-const c_220 U) (declare-const c_221 U)
+(declare-const c_222 U) (declare-const c_223 U)
+(declare-const c_224 U) (declare-const c_225 U)
+(declare-const c_226 U) (declare-const c_227 U)
+(declare-const c_228 U) (declare-const c_229 U)
+(declare-const c_230 U) (declare-const c_231 U)
+(declare-const c_232 U) (declare-const c_233 U)
+(declare-const c_234 U) (declare-const c_235 U)
+(declare-const c_236 U) (declare-const c_237 U)
+(declare-const c_238 U) (declare-const c_239 U)
+(declare-const c_240 U) (declare-const c_241 U)
+  
+(declare-fun b () Int)
+(declare-fun c () U)
+(assert (not (= (select (A c_184 c_185 c_186 c_187
+                          c_188 c_189 c_190 c_191 c_192
+                          c_193 c_194 c_195 c_196 c_197
+                          c_198 c_199 c_200 c_201 c_202
+                          c_203 c_204 c_205 c_206 c_207
+                          c_208 c_209 c_210 c_211 c_212
+                          c_213 c_214 c_215 c_216 c_217
+                          c_218 c_219 c_220 c_221 c_222
+                          c_223 c_224 c_225 c_226 c_227
+                          c_228 c_229 c_230 c_231 c_232
+                          c_233 c_234 c_235 c_236 c_237
+                          c_238 c_239 c_240 c_241) b) c)))
+(assert (and (= b 28) (= c c_212)))
+
+(check-sat)
diff --git a/test/regress/regress0/quantifiers/macro-subtype-param.smt2 b/test/regress/regress0/quantifiers/macro-subtype-param.smt2
new file mode 100644
index 000000000..20de79047
--- /dev/null
+++ b/test/regress/regress0/quantifiers/macro-subtype-param.smt2
@@ -0,0 +1,18 @@
+; COMMAND-LINE: --macros-quant
+; EXPECT: unknown
+; this will fail if type rule for APPLY_UF requires to be subtypes
+(set-logic ALL_SUPPORTED)
+
+(declare-datatypes (T) ((List (cons (hd T) (tl (List T))) (nil))))
+
+(declare-fun R ((List Int)) Bool)
+(assert (forall ((x (List Int))) (R x)))
+(declare-fun j1 () (List Real))
+(assert (not (R j1)))
+
+(declare-fun Q ((Array Real Int)) Bool)
+(assert (forall ((x (Array Real Int))) (Q x)))
+(declare-fun j2 () (Array Int Real))
+(assert (not (Q j2)))
+
+(check-sat)
diff --git a/test/regress/regress0/quantifiers/macros-real-arg.smt2 b/test/regress/regress0/quantifiers/macros-real-arg.smt2
new file mode 100644
index 000000000..675c96d68
--- /dev/null
+++ b/test/regress/regress0/quantifiers/macros-real-arg.smt2
@@ -0,0 +1,11 @@
+; COMMAND-LINE: --macros-quant
+; EXPECT: unsat
+; this will fail if type rule for APPLY_UF is made strict
+(set-logic UFLIRA)
+(declare-fun P (Int) Bool)
+(assert (forall ((x Int)) (P x)))
+(declare-fun k () Real)
+(declare-fun k2 () Int)
+(assert (or (not (P k)) (not (P k2))))
+(assert (= k 0))
+(check-sat)
diff --git a/test/regress/regress0/quantifiers/parametric-lists.smt2 b/test/regress/regress0/quantifiers/parametric-lists.smt2
new file mode 100644
index 000000000..c117934f8
--- /dev/null
+++ b/test/regress/regress0/quantifiers/parametric-lists.smt2
@@ -0,0 +1,42 @@
+(set-logic ALL_SUPPORTED)
+(set-info :status unsat)
+(declare-datatypes (T) ((List (cons (head T) (tail (List T))) (nil))))
+(declare-datatypes () ((KV (kv (key Int) (value Int)) (nilKV)))) ; key value pair
+(declare-fun mapper ((List Int)) (List KV))
+(assert
+  (forall
+    ((input (List Int)))
+     (ite
+        (= input (as nil (List Int)))
+        (= (as nil (List KV)) (mapper input))
+        (= (cons (kv 0 (head input)) (mapper (tail input))) (mapper input))
+     )
+  )                                                                                                                            
+)
+(declare-fun reduce ((List KV)) Int)
+(assert
+  (forall
+    ((inputk (List KV)))
+    (ite
+      (= inputk (as nil (List KV)))
+      (= 0 (reduce inputk))
+      (= (+ (value (head inputk)) (reduce (tail inputk))) (reduce inputk))
+    )
+  )
+)
+(declare-fun sum ((List Int)) Int)
+(assert
+  (forall
+    ((input (List Int)))
+    (ite
+      (= input (as nil (List Int)))
+      (= 0 (sum input))
+      (= (+ (head input) (sum (tail input))) (sum input))
+    )
+  )
+)
+(assert
+  (not (= (sum (cons 0 (as nil (List Int)))) (reduce (mapper (cons 0 (as nil (List Int)))))))
+)
+(check-sat)
+
diff --git a/test/regress/regress0/quantifiers/pure_dt_cbqi.smt2 b/test/regress/regress0/quantifiers/pure_dt_cbqi.smt2
new file mode 100644
index 000000000..a11d14e4a
--- /dev/null
+++ b/test/regress/regress0/quantifiers/pure_dt_cbqi.smt2
@@ -0,0 +1,6 @@
+(set-logic ALL_SUPPORTED)

+(set-info :status sat)

+(declare-datatypes () ((nat (Suc (pred nat)) (zero))))

+(declare-fun y () nat)

+(assert (forall ((x nat)) (not (= y (Suc x)))))

+(check-sat)

diff --git a/test/regress/regress0/quantifiers/qcf-rel-dom-opt.smt2 b/test/regress/regress0/quantifiers/qcf-rel-dom-opt.smt2
new file mode 100644
index 000000000..539f181af
--- /dev/null
+++ b/test/regress/regress0/quantifiers/qcf-rel-dom-opt.smt2
@@ -0,0 +1,45 @@
+(set-logic UFLIA)
+(set-info :status unsat)
+(declare-fun P (Int) Bool)
+
+(assert (P 0))
+(assert (P 1))
+(assert (P 2))
+(assert (P 3))
+(assert (P 4))
+(assert (P 5))
+(assert (P 6))
+(assert (P 7))
+(assert (P 8))
+(assert (P 9))
+
+(assert (P 10))
+(assert (P 11))
+(assert (P 12))
+(assert (P 13))
+(assert (P 14))
+(assert (P 15))
+(assert (P 16))
+(assert (P 17))
+(assert (P 18))
+(assert (P 19))
+
+(assert (P 20))
+(assert (P 21))
+(assert (P 22))
+(assert (P 23))
+(assert (P 24))
+(assert (P 25))
+(assert (P 26))
+(assert (P 27))
+(assert (P 28))
+(assert (P 29))
+
+(declare-fun Q (Int Int Int Int Int) Bool)
+(assert (forall ((x Int) (y Int) (z Int) (w Int) (q Int)) (or (not (P x)) (not (P y)) (not (P z)) (not (P w)) (not (P q)) (Q x y z w q))))
+
+(declare-fun R (Int) Bool)
+(assert (R 0))
+(assert (forall ((x Int)) (not (R x))))
+
+(check-sat)
diff --git a/test/regress/regress0/quantifiers/subtype-param-unk.smt2 b/test/regress/regress0/quantifiers/subtype-param-unk.smt2
new file mode 100644
index 000000000..836449cb9
--- /dev/null
+++ b/test/regress/regress0/quantifiers/subtype-param-unk.smt2
@@ -0,0 +1,19 @@
+; COMMAND-LINE: 
+; EXPECT: unknown
+; this will fail if type rule for APPLY_UF requires arguments to be subtypes
+(set-logic ALL_SUPPORTED)
+
+(declare-datatypes (T) ((List (cons (hd T) (tl (List T))) (nil))))
+
+(declare-fun R ((List Int)) Bool)
+
+(assert (forall ((x (List Int))) (R x)))
+(declare-fun j1 () (List Real))
+(assert (not (R j1)))
+
+(declare-fun Q ((Array Int Real)) Bool)
+(assert (forall ((x (Array Int Int))) (Q x)))
+(declare-fun j2 () (Array Int Real))
+(assert (not (Q j2)))
+
+(check-sat)
diff --git a/test/regress/regress0/quantifiers/subtype-param.smt2 b/test/regress/regress0/quantifiers/subtype-param.smt2
new file mode 100644
index 000000000..08615abf6
--- /dev/null
+++ b/test/regress/regress0/quantifiers/subtype-param.smt2
@@ -0,0 +1,16 @@
+(set-logic ALL_SUPPORTED)
+(set-info :status unsat)
+
+(declare-datatypes (T) ((List (cons (hd T) (tl (List T))) (nil))))
+
+(declare-fun R ((List Int)) Bool)
+(assert (forall ((x (List Real))) (R x)))
+
+(declare-fun Q ((Array Int Real)) Bool)
+(assert (forall ((x (Array Int Int))) (Q x)))
+
+(declare-fun k1 () (List Int))
+(declare-fun k2 () (Array Real Int))
+(assert (or (not (R k1)) (not (Q k2))))
+
+(check-sat)
diff --git a/test/regress/regress0/sets/card-2.smt2 b/test/regress/regress0/sets/card-2.smt2
new file mode 100644
index 000000000..cb414dbef
--- /dev/null
+++ b/test/regress/regress0/sets/card-2.smt2
@@ -0,0 +1,10 @@
+(set-logic QF_UFLIAFS)
+(declare-sort E 0)
+(declare-fun s () (Set E))
+(declare-fun t () (Set E))
+(declare-fun u () (Set E))
+(assert (>= (card s) 5))
+(assert (>= (card t) 5))
+(assert (<= (card u) 6))
+(assert (= u (union s t)))
+(check-sat)
diff --git a/test/regress/regress0/sets/card-3.smt2 b/test/regress/regress0/sets/card-3.smt2
new file mode 100644
index 000000000..949ed3457
--- /dev/null
+++ b/test/regress/regress0/sets/card-3.smt2
@@ -0,0 +1,11 @@
+(set-logic QF_UFLIAFS)
+(declare-sort E 0)
+(declare-fun s () (Set E))
+(declare-fun t () (Set E))
+(declare-fun u () (Set E))
+(assert (>= (card (union s t)) 8))
+(assert (>= (card (union s u)) 8))
+(assert (<= (card (union t u)) 5))
+(assert (<= (card s) 5))
+(assert (= (as emptyset (Set E)) (intersection t u)))
+(check-sat)
diff --git a/test/regress/regress0/sets/card-4.smt2 b/test/regress/regress0/sets/card-4.smt2
new file mode 100644
index 000000000..ea7fe42f3
--- /dev/null
+++ b/test/regress/regress0/sets/card-4.smt2
@@ -0,0 +1,23 @@
+(set-logic QF_UFLIAFS)
+(declare-sort E 0)
+(declare-fun s () (Set E))
+(declare-fun t () (Set E))
+(declare-fun u () (Set E))
+(assert (>= (card (union s t)) 8))
+(assert (>= (card (union s u)) 8))
+;(assert (<= (card (union t u)) 5))
+(assert (<= (card s) 5))
+(assert (= (as emptyset (Set E)) (intersection t u)))
+(declare-fun x1 () E)
+(declare-fun x2 () E)
+(declare-fun x3 () E)
+(declare-fun x4 () E)
+(declare-fun x5 () E)
+(declare-fun x6 () E)
+(assert (member x1 s))
+(assert (member x2 s))
+(assert (member x3 s))
+(assert (member x4 s))
+(assert (member x5 s))
+(assert (member x6 s))
+(check-sat)
diff --git a/test/regress/regress0/sets/card-5.smt2 b/test/regress/regress0/sets/card-5.smt2
new file mode 100644
index 000000000..65135e7b4
--- /dev/null
+++ b/test/regress/regress0/sets/card-5.smt2
@@ -0,0 +1,24 @@
+(set-logic QF_UFLIAFS)
+(declare-sort E 0)
+(declare-fun s () (Set E))
+(declare-fun t () (Set E))
+(declare-fun u () (Set E))
+(assert (>= (card (union s t)) 8))
+(assert (>= (card (union s u)) 8))
+;(assert (<= (card (union t u)) 5))
+(assert (<= (card s) 5))
+(assert (= (as emptyset (Set E)) (intersection t u)))
+(declare-fun x1 () E)
+(declare-fun x2 () E)
+(declare-fun x3 () E)
+(declare-fun x4 () E)
+(declare-fun x5 () E)
+(declare-fun x6 () E)
+(assert (member x1 s))
+(assert (member x2 s))
+(assert (member x3 s))
+(assert (member x4 s))
+(assert (member x5 s))
+(assert (member x6 s))
+(assert (distinct x1 x2 x3 x4 x5 x6))
+(check-sat)
diff --git a/test/regress/regress0/sets/card-6.smt2 b/test/regress/regress0/sets/card-6.smt2
new file mode 100644
index 000000000..1611952b7
--- /dev/null
+++ b/test/regress/regress0/sets/card-6.smt2
@@ -0,0 +1,16 @@
+(set-logic QF_UFLIAFS)
+(declare-sort E 0)
+(declare-fun A () (Set E))
+(declare-fun B () (Set E))
+(declare-fun C () (Set E))
+(assert
+  (and
+    (= (as emptyset (Set E))
+       (intersection A B))
+    (subset C (union A B))
+    (>= (card C) 5)
+    (<= (card A) 2)
+    (<= (card B) 2)
+  )
+)
+(check-sat)
diff --git a/test/regress/regress0/sets/card-7.smt2 b/test/regress/regress0/sets/card-7.smt2
new file mode 100644
index 000000000..94468dc57
--- /dev/null
+++ b/test/regress/regress0/sets/card-7.smt2
@@ -0,0 +1,46 @@
+(set-logic QF_UFLIAFS)
+(declare-sort E 0)
+(declare-fun A1 () (Set E))
+(declare-fun A2 () (Set E))
+(declare-fun A3 () (Set E))
+(declare-fun A4 () (Set E))
+(declare-fun A5 () (Set E))
+(declare-fun A6 () (Set E))
+(declare-fun A7 () (Set E))
+(declare-fun A8 () (Set E))
+(declare-fun A9 () (Set E))
+(declare-fun A10 () (Set E))
+(declare-fun A11 () (Set E))
+(declare-fun A12 () (Set E))
+(declare-fun A13 () (Set E))
+(declare-fun A14 () (Set E))
+(declare-fun A15 () (Set E))
+(declare-fun A16 () (Set E))
+(declare-fun A17 () (Set E))
+(declare-fun A18 () (Set E))
+(declare-fun A19 () (Set E))
+(declare-fun A20 () (Set E))
+(assert (and
+  (= (card A1) 1)
+  (= (card A2) 1)
+  (= (card A3) 1)
+  (= (card A4) 1)
+  (= (card A5) 1)
+  (= (card A6) 1)
+  (= (card A7) 1)
+  (= (card A8) 1)
+  (= (card A9) 1)
+  (= (card A10) 1)
+  (= (card A11) 1)
+  (= (card A12) 1)
+  (= (card A13) 1)
+  (= (card A14) 1)
+  (= (card A15) 1)
+  (= (card A16) 1)
+  (= (card A17) 1)
+  (= (card A18) 1)
+  (= (card A19) 1)
+  (= (card A20) 1)
+))
+(assert (= 20 (+ (card A1) (card A2) (card A3) (card A4) (card A5) (card A6) (card A7) (card A8) (card A9) (card A10) (card A11) (card A12) (card A13) (card A14) (card A15) (card A16) (card A17) (card A18) (card A19) (card A20))))
+(check-sat)
diff --git a/test/regress/regress0/sets/card.smt2 b/test/regress/regress0/sets/card.smt2
new file mode 100644
index 000000000..6b8c536d5
--- /dev/null
+++ b/test/regress/regress0/sets/card.smt2
@@ -0,0 +1,8 @@
+(set-logic QF_UFLIAFS)
+(declare-sort E 0)
+(declare-fun s () (Set E))
+(declare-fun t () (Set E))
+(assert (>= (card s) 5))
+(assert (>= (card t) 5))
+(assert (<= (card (union s t)) 4))
+(check-sat)
diff --git a/test/regress/regress0/strings/Makefile.am b/test/regress/regress0/strings/Makefile.am
index f5c6048e6..771b9f031 100644
--- a/test/regress/regress0/strings/Makefile.am
+++ b/test/regress/regress0/strings/Makefile.am
@@ -74,7 +74,9 @@ TESTS = \
   idof-handg.smt2 \
   fmf001.smt2 \
   type002.smt2 \
-  crash-1019.smt2
+  crash-1019.smt2 \
+  norn-31.smt2 \
+  strings-native-simple.cvc
 
 FAILING_TESTS =
 
diff --git a/test/regress/regress0/strings/norn-31.smt2 b/test/regress/regress0/strings/norn-31.smt2
new file mode 100644
index 000000000..4698f966f
--- /dev/null
+++ b/test/regress/regress0/strings/norn-31.smt2
@@ -0,0 +1,23 @@
+(set-logic QF_SLIA)
+(set-option :strings-exp true)
+(set-info :status unsat)
+
+(declare-fun var_0 () String)
+(declare-fun var_1 () String)
+(declare-fun var_2 () String)
+(declare-fun var_3 () String)
+(declare-fun var_4 () String)
+(declare-fun var_5 () String)
+(declare-fun var_6 () String)
+(declare-fun var_7 () String)
+(declare-fun var_8 () String)
+(declare-fun var_9 () String)
+(declare-fun var_10 () String)
+(declare-fun var_11 () String)
+(declare-fun var_12 () String)
+
+(assert (str.in.re var_1 (re.* (re.range "a" "u"))))
+(assert (str.in.re var_1 (re.++ (re.* (str.to.re "a")) (str.to.re "b"))))
+(assert (str.in.re var_1 (re.++ (re.++ (re.++ (re.* (re.union (str.to.re "a") (str.to.re "b"))) (str.to.re "b")) (str.to.re "a")) (re.* (re.union (str.to.re "a") (str.to.re "b"))))))
+(assert (not (str.in.re "" re.nostr)))
+(check-sat)
diff --git a/test/regress/regress0/strings/strings-native-simple.cvc b/test/regress/regress0/strings/strings-native-simple.cvc
new file mode 100644
index 000000000..568452e12
--- /dev/null
+++ b/test/regress/regress0/strings/strings-native-simple.cvc
@@ -0,0 +1,10 @@
+% EXPECT: sat
+
+x : STRING;
+y : STRING;
+
+ASSERT x = CONCAT( "abcd", y );
+ASSERT LENGTH( x ) >= 6;
+ASSERT LENGTH( y ) < 5;
+
+CHECKSAT;
diff --git a/test/regress/regress0/sygus/Makefile.am b/test/regress/regress0/sygus/Makefile.am
index 32caa4989..2ca807662 100644
--- a/test/regress/regress0/sygus/Makefile.am
+++ b/test/regress/regress0/sygus/Makefile.am
@@ -47,7 +47,8 @@ TESTS = commutative.sy \
         list-head-x.sy \
         clock-inc-tuple.sy \
         dt-test-ns.sy \
-        no-mention.sy
+        no-mention.sy \
+        max2-univ.sy
 
 # sygus tests currently taking too long for make regress
 EXTRA_DIST = $(TESTS) \
diff --git a/test/regress/regress0/sygus/max2-univ.sy b/test/regress/regress0/sygus/max2-univ.sy
new file mode 100644
index 000000000..3f8aac3b2
--- /dev/null
+++ b/test/regress/regress0/sygus/max2-univ.sy
@@ -0,0 +1,12 @@
+; EXPECT: unsat
+; COMMAND-LINE: --cegqi --no-dump-synth
+; Synthesize the maximum of 2 integers, but property has 4 variables (requires 2 passes)
+(set-logic LIA)
+(synth-fun max2 ((x Int) (y Int)) Int)
+(declare-var x Int)
+(declare-var y Int)
+(declare-var r Int)
+(declare-var w Int)
+(constraint (=> (< r 0) (=> (or (and (= x w) (= y (+ w r))) (and (= x (+ w r)) (= y w))) (= (max2 x y) w))))
+(check-synth)
+