diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-02-15 15:31:48 -0600 |
|---|---|---|
| committer | Aina Niemetz <aina.niemetz@gmail.com> | 2018-02-15 13:31:48 -0800 |
| commit | 55037e0bcef45c795f28ff3fcf6c1055af465c70 (patch) | |
| tree | 397d89bd10e541e1206c5dafdb8cf731feb34730 /test/regress/regress1/fmf | |
| parent | 52a39aca19b7238d08c3cebcfa46436a73194008 (diff) | |
Refactor regressions (#1581)
Diffstat (limited to 'test/regress/regress1/fmf')
42 files changed, 2446 insertions, 112 deletions
diff --git a/test/regress/regress1/fmf/ALG008-1.smt2 b/test/regress/regress1/fmf/ALG008-1.smt2 new file mode 100644 index 000000000..2c3bab80d --- /dev/null +++ b/test/regress/regress1/fmf/ALG008-1.smt2 @@ -0,0 +1,72 @@ +; COMMAND-LINE: --finite-model-find +; EXPECT: sat +;%-------------------------------------------------------------------------- +;% File : ALG008-1 : TPTP v5.4.0. Released v2.2.0. +;% Domain : General Algebra +;% Problem : TC + right identity does not give RC. +;% Version : [MP96] (equality) axioms : Especial. +;% English : An algebra with a right identity satisfying the Thomsen +;% Closure (RC) condition does not necessarily satisfy the +;% Reidemeister Closure (RC) condition. + +;% Refs : [McC98] McCune (1998), Email to G. Sutcliffe +;% : [MP96] McCune & Padmanabhan (1996), Automated Deduction in Eq +;% Source : [McC98] +;% Names : TC-3 [MP96] + +;% Status : Satisfiable +;% Rating : 0.50 v5.4.0, 0.80 v5.3.0, 0.78 v5.2.0, 0.80 v5.0.0, 0.78 v4.1.0, 0.71 v4.0.1, 0.80 v4.0.0, 0.50 v3.7.0, 0.33 v3.4.0, 0.50 v3.3.0, 0.33 v3.2.0, 0.80 v3.1.0, 0.67 v2.7.0, 0.33 v2.6.0, 0.86 v2.5.0, 0.50 v2.4.0, 0.67 v2.3.0, 1.00 v2.2.1 +;% Syntax : Number of clauses : 6 ( 0 non-Horn; 5 unit; 5 RR) +;% Number of atoms : 10 ( 10 equality) +;% Maximal clause size : 5 ( 2 average) +;% Number of predicates : 1 ( 0 propositional; 2-2 arity) +;% Number of functors : 9 ( 8 constant; 0-2 arity) +;% Number of variables : 9 ( 0 singleton) +;% Maximal term depth : 2 ( 2 average) +;% SPC : CNF_SAT_RFO_EQU_NUE + +;% Comments : The smallest model has 3 elements. +;%-------------------------------------------------------------------------- +;%----Thomsen Closure (TC) condition: +(set-logic UF) +(set-info :status sat) +(declare-sort sort__smt2 0) +; functions +(declare-fun multiply__smt2_2 ( sort__smt2 sort__smt2 ) sort__smt2) +(declare-fun identity__smt2_0 ( ) sort__smt2) +(declare-fun c4__smt2_0 ( ) sort__smt2) +(declare-fun a__smt2_0 ( ) sort__smt2) +(declare-fun c3__smt2_0 ( ) sort__smt2) +(declare-fun b__smt2_0 ( ) sort__smt2) +(declare-fun c2__smt2_0 ( ) sort__smt2) +(declare-fun c1__smt2_0 ( ) sort__smt2) +(declare-fun f__smt2_0 ( ) sort__smt2) +; predicates + +; thomsen_closure axiom +(assert (forall ((?V7 sort__smt2) (?V6 sort__smt2) (?W sort__smt2) (?V sort__smt2) (?U sort__smt2) (?Z sort__smt2) (?Y sort__smt2) (?X sort__smt2)) + (or (not (= (multiply__smt2_2 ?X ?Y) ?Z)) + (not (= (multiply__smt2_2 ?U ?V) ?Z)) + (not (= (multiply__smt2_2 ?X ?W) ?V6)) + (not (= (multiply__smt2_2 ?V7 ?V) ?V6)) + (= (multiply__smt2_2 ?U ?W) (multiply__smt2_2 ?V7 ?Y)))) ) + +;%----Right identity: +; right_identity axiom +(assert (forall ((?X sort__smt2)) (= (multiply__smt2_2 ?X identity__smt2_0) ?X)) ) + +;%----Denial of Reidimeister Closure (RC) condidition. +; prove_reidimeister1 negated_conjecture +(assert (= (multiply__smt2_2 c4__smt2_0 a__smt2_0) (multiply__smt2_2 c3__smt2_0 b__smt2_0)) ) + +; prove_reidimeister2 negated_conjecture +(assert (= (multiply__smt2_2 c2__smt2_0 a__smt2_0) (multiply__smt2_2 c1__smt2_0 b__smt2_0)) ) + +; prove_reidimeister3 negated_conjecture +(assert (= (multiply__smt2_2 c4__smt2_0 f__smt2_0) (multiply__smt2_2 c3__smt2_0 identity__smt2_0)) ) + +; prove_reidimeister4 negated_conjecture +(assert (not (= (multiply__smt2_2 c2__smt2_0 f__smt2_0) (multiply__smt2_2 c1__smt2_0 identity__smt2_0))) ) + + +(check-sat) diff --git a/test/regress/regress1/fmf/ForElimination-scala-9.smt2 b/test/regress/regress1/fmf/ForElimination-scala-9.smt2 deleted file mode 100644 index e8a784fc7..000000000 --- a/test/regress/regress1/fmf/ForElimination-scala-9.smt2 +++ /dev/null @@ -1,31 +0,0 @@ -; COMMAND-LINE: --finite-model-find --uf-ss=no-minimal --lang=smt2.5 -; 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/regress1/fmf/LeftistHeap.scala-8-ncm.smt2 b/test/regress/regress1/fmf/LeftistHeap.scala-8-ncm.smt2 new file mode 100644 index 000000000..a58e85c0d --- /dev/null +++ b/test/regress/regress1/fmf/LeftistHeap.scala-8-ncm.smt2 @@ -0,0 +1,33 @@ +; COMMAND-LINE: --finite-model-find --lang=smt2.5 +; 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/regress1/fmf/Makefile.am b/test/regress/regress1/fmf/Makefile.am index efaf535c6..dc07f6ca4 100644 --- a/test/regress/regress1/fmf/Makefile.am +++ b/test/regress/regress1/fmf/Makefile.am @@ -17,8 +17,45 @@ endif # If a test shouldn't be run in e.g. competition mode, # put it below in "TESTS +=" TESTS = \ - ForElimination-scala-9.smt2 \ - nunchaku2309663.nun.min.smt2 + agree466.smt2 \ + ALG008-1.smt2 \ + bug0909.smt2 \ + bug764.smt2 \ + datatypes-ufinite.smt2 \ + datatypes-ufinite-nested.smt2 \ + fc-pigeonhole19.smt2 \ + fib-core.smt2 \ + fmf-bound-2dim.smt2 \ + fmf-fun-no-elim-ext-arith2.smt2 \ + fmf-strange-bounds.smt2 \ + issue916-fmf-or.smt2 \ + jasmin-cdt-crash.smt2 \ + LeftistHeap.scala-8-ncm.smt2 \ + lst-no-self-rev-exp.smt2 \ + nun-0208-to.smt2 \ + pow2-bool.smt2 \ + with-ind-104-core.smt2 \ + agree467.smt2 \ + alg202+1.smt2 \ + am-bad-model.cvc \ + bound-int-alt.smt2 \ + bug651.smt2 \ + bug723-irrelevant-funs.smt2 \ + cons-sets-bounds.smt2 \ + constr-ground-to.smt2 \ + dt-proper-model.smt2 \ + fmf-bound-int.smt2 \ + fmf-fun-no-elim-ext-arith.smt2 \ + forall_unit_data.smt2 \ + fore19-exp2-core.smt2 \ + german169.smt2 \ + german73.smt2 \ + ko-bound-set.cvc \ + loopy_coda.smt2 \ + memory_model-R_cpp-dd.cvc \ + PUZ001+1.smt2 \ + refcount24.cvc.smt2 \ + sc-crash-052316.smt2 EXTRA_DIST = $(TESTS) diff --git a/test/regress/regress1/fmf/PUZ001+1.smt2 b/test/regress/regress1/fmf/PUZ001+1.smt2 new file mode 100644 index 000000000..f3db78491 --- /dev/null +++ b/test/regress/regress1/fmf/PUZ001+1.smt2 @@ -0,0 +1,118 @@ +; COMMAND-LINE: --finite-model-find --no-check-proofs --no-check-unsat-core +; EXPECT: unsat +;%------------------------------------------------------------------------------ +;% File : PUZ001+1 : TPTP v5.4.0. Released v2.0.0. +;% Domain : Puzzles +;% Problem : Dreadbury Mansion +;% Version : Especial. +;% Theorem formulation : Reduced > Complete. +;% English : Someone who lives in Dreadbury Mansion killed Aunt Agatha. +;% Agatha, the butler, and Charles live in Dreadbury Mansion, +;% and are the only people who live therein. A killer always +;% hates his victim, and is never richer than his victim. +;% Charles hates no one that Aunt Agatha hates. Agatha hates +;% everyone except the butler. The butler hates everyone not +;% richer than Aunt Agatha. The butler hates everyone Aunt +;% Agatha hates. No one hates everyone. Agatha is not the +;% butler. Therefore : Agatha killed herself. + +;% Refs : [Pel86] Pelletier (1986), Seventy-five Problems for Testing Au +;% : [Hah94] Haehnle (1994), Email to G. Sutcliffe +;% Source : [Hah94] +;% Names : Pelletier 55 [Pel86] + +;% Status : Theorem +;% Rating : 0.07 v5.3.0, 0.19 v5.2.0, 0.00 v5.0.0, 0.08 v4.1.0, 0.13 v4.0.0, 0.12 v3.7.0, 0.14 v3.5.0, 0.00 v3.4.0, 0.08 v3.3.0, 0.11 v3.2.0, 0.22 v3.1.0, 0.17 v2.7.0, 0.00 v2.5.0, 0.33 v2.4.0, 0.33 v2.2.1, 0.00 v2.1.0 +;% Syntax : Number of formulae : 14 ( 6 unit) +;% Number of atoms : 24 ( 5 equality) +;% Maximal formula depth : 5 ( 3 average) +;% Number of connectives : 16 ( 6 ~; 2 |; 1 &) +;% ( 0 <=>; 7 =>; 0 <=; 0 <~>) +;% ( 0 ~|; 0 ~&) +;% Number of predicates : 5 ( 0 propositional; 1-2 arity) +;% Number of functors : 3 ( 3 constant; 0-0 arity) +;% Number of variables : 12 ( 0 sgn; 10 !; 2 ?) +;% Maximal term depth : 1 ( 1 average) +;% SPC : FOF_THM_RFO_SEQ + +;% Comments : Modified by Geoff Sutcliffe. +;% : Also known as "Who killed Aunt Agatha" +;%------------------------------------------------------------------------------ +;%----Problem axioms +(set-logic UF) +(set-info :status unsat) +(declare-sort sort__smt2 0) +; functions +(declare-fun agatha__smt2_0 ( ) sort__smt2) +(declare-fun butler__smt2_0 ( ) sort__smt2) +(declare-fun charles__smt2_0 ( ) sort__smt2) +; predicates +(declare-fun lives__smt2_1 ( sort__smt2 ) Bool) +(declare-fun killed__smt2_2 ( sort__smt2 sort__smt2 ) Bool) +(declare-fun hates__smt2_2 ( sort__smt2 sort__smt2 ) Bool) +(declare-fun richer__smt2_2 ( sort__smt2 sort__smt2 ) Bool) + +; pel55_1 axiom +(assert (exists ((?X sort__smt2)) + (and (lives__smt2_1 ?X) + (killed__smt2_2 ?X agatha__smt2_0)))) + +; pel55_2_1 axiom +(assert (lives__smt2_1 agatha__smt2_0)) + +; pel55_2_2 axiom +(assert (lives__smt2_1 butler__smt2_0)) + +; pel55_2_3 axiom +(assert (lives__smt2_1 charles__smt2_0)) + +; pel55_3 axiom +(assert (forall ((?X sort__smt2)) + (=> (lives__smt2_1 ?X) + (or (= ?X agatha__smt2_0) + (= ?X butler__smt2_0) + (= ?X charles__smt2_0))))) + +; pel55_4 axiom +(assert (forall ((?X sort__smt2) (?Y sort__smt2)) + (=> (killed__smt2_2 ?X ?Y) + (hates__smt2_2 ?X ?Y)))) + +; pel55_5 axiom +(assert (forall ((?X sort__smt2) (?Y sort__smt2)) + (=> (killed__smt2_2 ?X ?Y) + (not (richer__smt2_2 ?X ?Y))))) + +; pel55_6 axiom +(assert (forall ((?X sort__smt2)) + (=> (hates__smt2_2 agatha__smt2_0 ?X) + (not (hates__smt2_2 charles__smt2_0 ?X))))) + +; pel55_7 axiom +(assert (forall ((?X sort__smt2)) + (=> (not (= ?X butler__smt2_0)) + (hates__smt2_2 agatha__smt2_0 ?X)))) + +; pel55_8 axiom +(assert (forall ((?X sort__smt2)) + (=> (not (richer__smt2_2 ?X agatha__smt2_0)) + (hates__smt2_2 butler__smt2_0 ?X)))) + +; pel55_9 axiom +(assert (forall ((?X sort__smt2)) + (=> (hates__smt2_2 agatha__smt2_0 ?X) + (hates__smt2_2 butler__smt2_0 ?X)))) + +; pel55_10 axiom +(assert (forall ((?X sort__smt2)) +(exists ((?Y sort__smt2)) (not (hates__smt2_2 ?X ?Y))))) + +; pel55_11 axiom +(assert (not (= agatha__smt2_0 butler__smt2_0))) + +;----This is the conjecture with negated conjecture +; pel55 conjecture +(assert (not (killed__smt2_2 agatha__smt2_0 agatha__smt2_0))) + + +(check-sat) diff --git a/test/regress/regress1/fmf/agree466.smt2 b/test/regress/regress1/fmf/agree466.smt2 new file mode 100644 index 000000000..d17a663c6 --- /dev/null +++ b/test/regress/regress1/fmf/agree466.smt2 @@ -0,0 +1,474 @@ +; COMMAND-LINE: --finite-model-find --lang=smt2.5 +; EXPECT: sat +; Preamble -------------- +(set-logic ALL_SUPPORTED) +(set-info :status sat) +(declare-datatypes () ((UNIT (Unit)))) +(declare-datatypes () ((BOOL (Truth) (Falsity)))) + +; Decls -------------- +(declare-sort node$type 0) +(declare-sort value$type 0) +(define-sort Nodes$elem$type () node$type) +(declare-sort Nodes$t$type 0) +(declare-fun Nodes$empty () Nodes$t$type) +(declare-fun Nodes$mem (Nodes$elem$type Nodes$t$type) BOOL) +(declare-fun Nodes$add (Nodes$elem$type Nodes$t$type) Nodes$t$type) +(declare-fun Nodes$remove (Nodes$elem$type Nodes$t$type) Nodes$t$type) +(declare-fun Nodes$cardinality (Nodes$t$type) Int) +(declare-fun Nodes$union (Nodes$t$type Nodes$t$type) Nodes$t$type) +(declare-fun Nodes$disjoint (Nodes$t$type Nodes$t$type) BOOL) +;Nodes$disjoint_empty : +(assert (forall ((a Nodes$t$type)) (= (Nodes$disjoint a Nodes$empty) Truth))) +;Nodes$disjoint_comm : +(assert (forall ((a Nodes$t$type) (b Nodes$t$type)) (= (Nodes$disjoint a b) + (Nodes$disjoint b a)))) +;Nodes$mem_empty : +(assert (forall ((e Nodes$elem$type)) (not (= (Nodes$mem e Nodes$empty) + Truth)))) +;Nodes$mem_add : +(assert (forall ((x Nodes$elem$type) (y Nodes$elem$type) (s Nodes$t$type)) + (= (Nodes$mem x (Nodes$add y s)) (ite (or (= x y) (= (Nodes$mem x s) + Truth)) Truth + Falsity)))) +;Nodes$mem_remove : +(assert (forall ((x Nodes$elem$type) (y Nodes$elem$type) (s Nodes$t$type)) + (= (Nodes$mem x (Nodes$remove y s)) (ite (and (not (= x y)) (= + (Nodes$mem + x s) + Truth)) + Truth Falsity)))) +;Nodes$mem_union1 : +(assert (forall ((x Nodes$elem$type) (a Nodes$t$type)) (=> (= (Nodes$mem x a) + Truth) (forall + ((b Nodes$t$type)) + (= + (Nodes$mem + x (Nodes$union + a b)) + Truth))))) +;Nodes$mem_union2 : +(assert (forall ((a Nodes$t$type) (b Nodes$t$type)) (= (Nodes$union a b) + (Nodes$union b a)))) +;Nodes$mem_union3 : +(assert (forall ((x Nodes$elem$type) (a Nodes$t$type) (b Nodes$t$type)) + (=> (= (Nodes$mem x (Nodes$union a b)) Truth) (or (= (Nodes$mem x a) + Truth) (= (Nodes$mem + x b) + Truth))))) +;Nodes$mem_union4 : +(assert (forall ((a Nodes$t$type)) (= (Nodes$union a a) a))) +;Nodes$mem_union5 : +(assert (forall ((a Nodes$t$type)) (= (Nodes$union a Nodes$empty) a))) +;Nodes$empty_union : +(assert (forall ((a Nodes$t$type) (b Nodes$t$type)) (=> (= (Nodes$union a b) + Nodes$empty) + (= a Nodes$empty)))) +;Nodes$card_empty : +(assert (= (Nodes$cardinality Nodes$empty) 0)) +;Nodes$card_zero : +(assert (forall ((s Nodes$t$type)) (=> (= (Nodes$cardinality s) 0) (= + s + Nodes$empty)))) +;Nodes$card_non_negative : +(assert (forall ((s Nodes$t$type)) (>= (Nodes$cardinality s) 0))) +;Nodes$card_add : +(assert (forall ((x Nodes$elem$type) (s Nodes$t$type)) (= (Nodes$cardinality + (Nodes$add x s)) + (ite (= (Nodes$mem + x s) Truth) + (Nodes$cardinality + s) (+ (Nodes$cardinality + s) 1))))) +;Nodes$card_remove : +(assert (forall ((x Nodes$elem$type) (s Nodes$t$type)) (= (Nodes$cardinality + (Nodes$remove x s)) + (ite (= (Nodes$mem + x s) Truth) (- + (Nodes$cardinality + s) 1) (Nodes$cardinality + s))))) +;Nodes$card_union : +(assert (forall ((a Nodes$t$type) (b Nodes$t$type)) (=> (= (Nodes$disjoint + a b) Truth) + (= (Nodes$cardinality + (Nodes$union a b)) (+ + (Nodes$cardinality + a) (Nodes$cardinality b)))))) +(declare-fun Nodes$eq (Nodes$t$type Nodes$t$type) BOOL) +;Nodes$eq_is_equality : +(assert (forall ((a Nodes$t$type) (b Nodes$t$type)) (= (Nodes$eq a b) + (ite (= a b) Truth + Falsity)))) +;Nodes$equal1 : +(assert (forall ((a Nodes$t$type) (b Nodes$t$type)) (=> (forall ((x Nodes$elem$type)) + (= (Nodes$mem x a) + (Nodes$mem x b))) + (= (Nodes$eq a b) + Truth)))) +(define-sort Values$elem$type () value$type) +(declare-sort Values$t$type 0) +(declare-fun Values$empty () Values$t$type) +(declare-fun Values$mem (Values$elem$type Values$t$type) BOOL) +(declare-fun Values$add (Values$elem$type Values$t$type) Values$t$type) +(declare-fun Values$remove (Values$elem$type Values$t$type) Values$t$type) +(declare-fun Values$cardinality (Values$t$type) Int) +(declare-fun Values$union (Values$t$type Values$t$type) Values$t$type) +(declare-fun Values$disjoint (Values$t$type Values$t$type) BOOL) +;Values$disjoint_empty : +(assert (forall ((a Values$t$type)) (= (Values$disjoint a Values$empty) + Truth))) +;Values$disjoint_comm : +(assert (forall ((a Values$t$type) (b Values$t$type)) (= (Values$disjoint + a b) (Values$disjoint + b a)))) +;Values$mem_empty : +(assert (forall ((e Values$elem$type)) (not (= (Values$mem e Values$empty) + Truth)))) +;Values$mem_add : +(assert (forall ((x Values$elem$type) (y Values$elem$type) (s Values$t$type)) + (= (Values$mem x (Values$add y s)) (ite (or (= x y) (= (Values$mem + x s) Truth)) + Truth Falsity)))) +;Values$mem_remove : +(assert (forall ((x Values$elem$type) (y Values$elem$type) (s Values$t$type)) + (= (Values$mem x (Values$remove y s)) (ite (and (not (= x y)) + (= (Values$mem x s) + Truth)) Truth Falsity)))) +;Values$mem_union1 : +(assert (forall ((x Values$elem$type) (a Values$t$type)) (=> (= (Values$mem + x a) + Truth) (forall + ( + (b Values$t$type)) + (= + (Values$mem + x + (Values$union + a b)) + Truth))))) +;Values$mem_union2 : +(assert (forall ((a Values$t$type) (b Values$t$type)) (= (Values$union a b) + (Values$union b a)))) +;Values$mem_union3 : +(assert (forall ((x Values$elem$type) (a Values$t$type) (b Values$t$type)) + (=> (= (Values$mem x (Values$union a b)) Truth) (or (= (Values$mem + x a) Truth) + (= (Values$mem x b) + Truth))))) +;Values$mem_union4 : +(assert (forall ((a Values$t$type)) (= (Values$union a a) a))) +;Values$mem_union5 : +(assert (forall ((a Values$t$type)) (= (Values$union a Values$empty) a))) +;Values$empty_union : +(assert (forall ((a Values$t$type) (b Values$t$type)) (=> (= (Values$union + a b) Values$empty) + (= a Values$empty)))) +;Values$card_empty : +(assert (= (Values$cardinality Values$empty) 0)) +;Values$card_zero : +(assert (forall ((s Values$t$type)) (=> (= (Values$cardinality s) 0) + (= s Values$empty)))) +;Values$card_non_negative : +(assert (forall ((s Values$t$type)) (>= (Values$cardinality s) 0))) +;Values$card_add : +(assert (forall ((x Values$elem$type) (s Values$t$type)) (= (Values$cardinality + (Values$add x s)) + (ite (= (Values$mem + x s) + Truth) + (Values$cardinality + s) (+ (Values$cardinality + s) 1))))) +;Values$card_remove : +(assert (forall ((x Values$elem$type) (s Values$t$type)) (= (Values$cardinality + (Values$remove + x s)) (ite + (= + (Values$mem + x s) + Truth) (- + (Values$cardinality + s) + 1) + (Values$cardinality + s))))) +;Values$card_union : +(assert (forall ((a Values$t$type) (b Values$t$type)) (=> (= (Values$disjoint + a b) Truth) + (= (Values$cardinality + (Values$union a b)) (+ + (Values$cardinality + a) (Values$cardinality + b)))))) +(declare-fun Values$eq (Values$t$type Values$t$type) BOOL) +;Values$eq_is_equality : +(assert (forall ((a Values$t$type) (b Values$t$type)) (= (Values$eq a b) + (ite (= a b) Truth + Falsity)))) +;Values$equal1 : +(assert (forall ((a Values$t$type) (b Values$t$type)) (=> (forall ((x Values$elem$type)) + (= (Values$mem x a) + (Values$mem + x b))) (= (Values$eq + a b) + Truth)))) +(define-sort node_set$type () (Array node$type BOOL)) +(declare-fun mk_array_1 () (Array node$type BOOL)) +;mk_array_1_def : +(assert (forall ((mk_array_1_index node$type)) (= (select mk_array_1 + mk_array_1_index) Falsity))) +(define-fun empty_node_set () node_set$type mk_array_1) +(define-sort node_pair_set$type () (Array node$type (Array node$type BOOL))) +(declare-fun mk_array_2 () (Array node$type BOOL)) +;mk_array_2_def : +(assert (forall ((mk_array_2_index node$type)) (= (select mk_array_2 + mk_array_2_index) Falsity))) +(declare-fun mk_array_3 () (Array node$type (Array node$type BOOL))) +;mk_array_3_def : +(assert (forall ((mk_array_3_index node$type)) (= (select mk_array_3 + mk_array_3_index) mk_array_2))) +(define-fun empty_node_pair_set () node_pair_set$type mk_array_3) +(declare-fun mk_array_4 () (Array node$type BOOL)) +;mk_array_4_def : +(assert (forall ((mk_array_4_index node$type)) (= (select mk_array_4 + mk_array_4_index) Truth))) +(declare-fun mk_array_5 () (Array node$type (Array node$type BOOL))) +;mk_array_5_def : +(assert (forall ((mk_array_5_index node$type)) (= (select mk_array_5 + mk_array_5_index) mk_array_4))) +(define-fun full_node_pair_set () node_pair_set$type mk_array_5) +(declare-fun input () (Array node$type value$type)) +(declare-fun t () Int) +;positive_bound : +(assert (> t 0)) +(define-sort message$type () Values$t$type) +(define-sort message_set$type () (Array node$type message$type)) +(define-sort state$type () Values$t$type) +(define-sort state_set$type () (Array node$type state$type)) +(define-fun null_message () message$type Values$empty) +(declare-fun mk_array_6 () (Array node$type message$type)) +;mk_array_6_def : +(assert (forall ((mk_array_6_index node$type)) (= (select mk_array_6 + mk_array_6_index) null_message))) +(define-fun null_message_set () message_set$type mk_array_6) +(define-fun null_state () state$type Values$empty) +(declare-fun mk_array_7 () (Array node$type state$type)) +;mk_array_7_def : +(assert (forall ((mk_array_7_index node$type)) (= (select mk_array_7 + mk_array_7_index) null_state))) +(define-fun null_state_set () state_set$type mk_array_7) +(declare-fun choose (Values$t$type) value$type) +;choosen_value : +(assert (forall ((vals Values$t$type)) (or (= vals Values$empty) (= (Values$mem + (choose + vals) + vals) + Truth)))) +(define-sort failure_pattern$type () node_pair_set$type) +(define-fun is_faulty ((p node$type) (deliver failure_pattern$type)) BOOL +(ite (exists ((q node$type)) (not (= (select (select deliver p) q) Truth))) +Truth Falsity)) +(define-fun is_silent ((p node$type) (deliver failure_pattern$type)) BOOL +(ite (forall ((q node$type)) (not (= (select (select deliver p) q) Truth))) +Truth Falsity)) +(declare-datatypes () ((phase_state$type (init_phase) (send_phase) (recv_phase) (comp_phase)))) +(declare-datatypes () ((clean_state$type (before) (active) (after)))) + +; Var Decls -------------- +(declare-fun my_compute$result$1 () state$type) +(declare-fun output$1 () (Array node$type value$type)) +(declare-fun comp_done () node_set$type) +(declare-fun compute$can_decide$0$1 () BOOL) +(declare-fun chosen () (Array node$type BOOL)) +(declare-fun recv_done () node_pair_set$type) +(declare-fun output () (Array node$type value$type)) +(declare-fun phase () phase_state$type) +(declare-fun global_state () state_set$type) +(declare-fun my_decide$result$1 () value$type) +(declare-fun round () Int) +(declare-fun compute$n () node$type) +(declare-fun send_done () node_pair_set$type) +(declare-fun my_can_decide$result$1 () BOOL) +(declare-fun chosen$1 () (Array node$type BOOL)) +(declare-fun comp_done$1 () node_set$type) +(declare-fun global_state$1 () state_set$type) + +; Asserts -------------- +(assert (not (=> (forall ((n node$type)) (=> + (and + (= + (select + chosen + n) + Truth) + (= + round (+ + t + 1))) + (and + (forall + ( + (n node$type) (m node$type)) + (= + (select + (select + send_done + n) + m) + Truth)) + (forall + ( + (n node$type) (m node$type)) + (= + (select + (select + recv_done + n) + m) + Truth))))) + (=> (= phase comp_phase) (=> + (not + (= (select + comp_done + compute$n) + Truth)) + (=> + (= my_compute$result$1 + (select + global_state + compute$n)) + (=> + (= global_state$1 + (store + global_state + compute$n + my_compute$result$1)) + (=> + (= my_can_decide$result$1 + (ite + (= round (+ + t 1)) + Truth + Falsity)) + (=> + (= compute$can_decide$0$1 + my_can_decide$result$1) + (= (ite + (= + compute$can_decide$0$1 + Truth) + (ite + (=> + (= + my_decide$result$1 + (choose + (select + global_state$1 + compute$n))) + (=> + (= + output$1 + (store + output + compute$n + my_decide$result$1)) + (=> + (= + chosen$1 + (store + chosen + compute$n + Truth)) + (=> + (= + comp_done$1 + (store + comp_done + compute$n + Truth)) + (forall + ( + (n node$type)) + (=> + (and + (= + (select + chosen$1 + n) + Truth) + (= + round (+ + t + 1))) + (and + (forall + ( + (n node$type) (m node$type)) + (= + (select + (select + send_done + n) + m) + Truth)) + (forall + ( + (n node$type) (m node$type)) + (= + (select + (select + recv_done + n) + m) + Truth))))))))) + Truth + Falsity) + (ite + (=> + (= + comp_done$1 + (store + comp_done + compute$n + Truth)) + (forall + ( + (n node$type)) + (=> + (and + (= + (select + chosen + n) + Truth) + (= + round (+ + t + 1))) + (and + (forall + ( + (n node$type) (m node$type)) + (= + (select + (select + send_done + n) + m) + Truth)) + (forall + ( + (n node$type) (m node$type)) + (= + (select + (select + recv_done + n) + m) + Truth)))))) + Truth + Falsity)) + Truth)))))))))) + +(check-sat) diff --git a/test/regress/regress1/fmf/agree467.smt2 b/test/regress/regress1/fmf/agree467.smt2 new file mode 100644 index 000000000..07180cf4f --- /dev/null +++ b/test/regress/regress1/fmf/agree467.smt2 @@ -0,0 +1,341 @@ +; COMMAND-LINE: --finite-model-find --lang=smt2.5 +; EXPECT: unsat +; Preamble -------------- +(set-logic ALL_SUPPORTED) +(set-info :status unsat) +(declare-datatypes () ((UNIT (Unit)))) +(declare-datatypes () ((BOOL (Truth) (Falsity)))) + +; Decls -------------- +(declare-sort node$type 0) +(declare-sort value$type 0) +(define-sort Nodes$elem$type () node$type) +(declare-sort Nodes$t$type 0) +(declare-fun Nodes$empty () Nodes$t$type) +(declare-fun Nodes$mem (Nodes$elem$type Nodes$t$type) BOOL) +(declare-fun Nodes$add (Nodes$elem$type Nodes$t$type) Nodes$t$type) +(declare-fun Nodes$remove (Nodes$elem$type Nodes$t$type) Nodes$t$type) +(declare-fun Nodes$cardinality (Nodes$t$type) Int) +(declare-fun Nodes$union (Nodes$t$type Nodes$t$type) Nodes$t$type) +(declare-fun Nodes$disjoint (Nodes$t$type Nodes$t$type) BOOL) +;Nodes$disjoint_empty : +(assert (forall ((a Nodes$t$type)) (= (Nodes$disjoint a Nodes$empty) Truth))) +;Nodes$disjoint_comm : +(assert (forall ((a Nodes$t$type) (b Nodes$t$type)) (= (Nodes$disjoint a b) + (Nodes$disjoint b a)))) +;Nodes$mem_empty : +(assert (forall ((e Nodes$elem$type)) (not (= (Nodes$mem e Nodes$empty) + Truth)))) +;Nodes$mem_add : +(assert (forall ((x Nodes$elem$type) (y Nodes$elem$type) (s Nodes$t$type)) + (= (Nodes$mem x (Nodes$add y s)) (ite (or (= x y) (= (Nodes$mem x s) + Truth)) Truth + Falsity)))) +;Nodes$mem_remove : +(assert (forall ((x Nodes$elem$type) (y Nodes$elem$type) (s Nodes$t$type)) + (= (Nodes$mem x (Nodes$remove y s)) (ite (and (not (= x y)) (= + (Nodes$mem + x s) + Truth)) + Truth Falsity)))) +;Nodes$mem_union1 : +(assert (forall ((x Nodes$elem$type) (a Nodes$t$type)) (=> (= (Nodes$mem x a) + Truth) (forall + ((b Nodes$t$type)) + (= + (Nodes$mem + x (Nodes$union + a b)) + Truth))))) +;Nodes$mem_union2 : +(assert (forall ((a Nodes$t$type) (b Nodes$t$type)) (= (Nodes$union a b) + (Nodes$union b a)))) +;Nodes$mem_union3 : +(assert (forall ((x Nodes$elem$type) (a Nodes$t$type) (b Nodes$t$type)) + (=> (= (Nodes$mem x (Nodes$union a b)) Truth) (or (= (Nodes$mem x a) + Truth) (= (Nodes$mem + x b) + Truth))))) +;Nodes$mem_union4 : +(assert (forall ((a Nodes$t$type)) (= (Nodes$union a a) a))) +;Nodes$mem_union5 : +(assert (forall ((a Nodes$t$type)) (= (Nodes$union a Nodes$empty) a))) +;Nodes$empty_union : +(assert (forall ((a Nodes$t$type) (b Nodes$t$type)) (=> (= (Nodes$union a b) + Nodes$empty) + (= a Nodes$empty)))) +;Nodes$card_empty : +(assert (= (Nodes$cardinality Nodes$empty) 0)) +;Nodes$card_zero : +(assert (forall ((s Nodes$t$type)) (=> (= (Nodes$cardinality s) 0) (= + s + Nodes$empty)))) +;Nodes$card_non_negative : +(assert (forall ((s Nodes$t$type)) (>= (Nodes$cardinality s) 0))) +;Nodes$card_add : +(assert (forall ((x Nodes$elem$type) (s Nodes$t$type)) (= (Nodes$cardinality + (Nodes$add x s)) + (ite (= (Nodes$mem + x s) Truth) + (Nodes$cardinality + s) (+ (Nodes$cardinality + s) 1))))) +;Nodes$card_remove : +(assert (forall ((x Nodes$elem$type) (s Nodes$t$type)) (= (Nodes$cardinality + (Nodes$remove x s)) + (ite (= (Nodes$mem + x s) Truth) (- + (Nodes$cardinality + s) 1) (Nodes$cardinality + s))))) +;Nodes$card_union : +(assert (forall ((a Nodes$t$type) (b Nodes$t$type)) (=> (= (Nodes$disjoint + a b) Truth) + (= (Nodes$cardinality + (Nodes$union a b)) (+ + (Nodes$cardinality + a) (Nodes$cardinality b)))))) +(declare-fun Nodes$eq (Nodes$t$type Nodes$t$type) BOOL) +;Nodes$eq_is_equality : +(assert (forall ((a Nodes$t$type) (b Nodes$t$type)) (= (Nodes$eq a b) + (ite (= a b) Truth + Falsity)))) +;Nodes$equal1 : +(assert (forall ((a Nodes$t$type) (b Nodes$t$type)) (=> (forall ((x Nodes$elem$type)) + (= (Nodes$mem x a) + (Nodes$mem x b))) + (= (Nodes$eq a b) + Truth)))) +(define-sort Values$elem$type () value$type) +(declare-sort Values$t$type 0) +(declare-fun Values$empty () Values$t$type) +(declare-fun Values$mem (Values$elem$type Values$t$type) BOOL) +(declare-fun Values$add (Values$elem$type Values$t$type) Values$t$type) +(declare-fun Values$remove (Values$elem$type Values$t$type) Values$t$type) +(declare-fun Values$cardinality (Values$t$type) Int) +(declare-fun Values$union (Values$t$type Values$t$type) Values$t$type) +(declare-fun Values$disjoint (Values$t$type Values$t$type) BOOL) +;Values$disjoint_empty : +(assert (forall ((a Values$t$type)) (= (Values$disjoint a Values$empty) + Truth))) +;Values$disjoint_comm : +(assert (forall ((a Values$t$type) (b Values$t$type)) (= (Values$disjoint + a b) (Values$disjoint + b a)))) +;Values$mem_empty : +(assert (forall ((e Values$elem$type)) (not (= (Values$mem e Values$empty) + Truth)))) +;Values$mem_add : +(assert (forall ((x Values$elem$type) (y Values$elem$type) (s Values$t$type)) + (= (Values$mem x (Values$add y s)) (ite (or (= x y) (= (Values$mem + x s) Truth)) + Truth Falsity)))) +;Values$mem_remove : +(assert (forall ((x Values$elem$type) (y Values$elem$type) (s Values$t$type)) + (= (Values$mem x (Values$remove y s)) (ite (and (not (= x y)) + (= (Values$mem x s) + Truth)) Truth Falsity)))) +;Values$mem_union1 : +(assert (forall ((x Values$elem$type) (a Values$t$type)) (=> (= (Values$mem + x a) + Truth) (forall + ( + (b Values$t$type)) + (= + (Values$mem + x + (Values$union + a b)) + Truth))))) +;Values$mem_union2 : +(assert (forall ((a Values$t$type) (b Values$t$type)) (= (Values$union a b) + (Values$union b a)))) +;Values$mem_union3 : +(assert (forall ((x Values$elem$type) (a Values$t$type) (b Values$t$type)) + (=> (= (Values$mem x (Values$union a b)) Truth) (or (= (Values$mem + x a) Truth) + (= (Values$mem x b) + Truth))))) +;Values$mem_union4 : +(assert (forall ((a Values$t$type)) (= (Values$union a a) a))) +;Values$mem_union5 : +(assert (forall ((a Values$t$type)) (= (Values$union a Values$empty) a))) +;Values$empty_union : +(assert (forall ((a Values$t$type) (b Values$t$type)) (=> (= (Values$union + a b) Values$empty) + (= a Values$empty)))) +;Values$card_empty : +(assert (= (Values$cardinality Values$empty) 0)) +;Values$card_zero : +(assert (forall ((s Values$t$type)) (=> (= (Values$cardinality s) 0) + (= s Values$empty)))) +;Values$card_non_negative : +(assert (forall ((s Values$t$type)) (>= (Values$cardinality s) 0))) +;Values$card_add : +(assert (forall ((x Values$elem$type) (s Values$t$type)) (= (Values$cardinality + (Values$add x s)) + (ite (= (Values$mem + x s) + Truth) + (Values$cardinality + s) (+ (Values$cardinality + s) 1))))) +;Values$card_remove : +(assert (forall ((x Values$elem$type) (s Values$t$type)) (= (Values$cardinality + (Values$remove + x s)) (ite + (= + (Values$mem + x s) + Truth) (- + (Values$cardinality + s) + 1) + (Values$cardinality + s))))) +;Values$card_union : +(assert (forall ((a Values$t$type) (b Values$t$type)) (=> (= (Values$disjoint + a b) Truth) + (= (Values$cardinality + (Values$union a b)) (+ + (Values$cardinality + a) (Values$cardinality + b)))))) +(declare-fun Values$eq (Values$t$type Values$t$type) BOOL) +;Values$eq_is_equality : +(assert (forall ((a Values$t$type) (b Values$t$type)) (= (Values$eq a b) + (ite (= a b) Truth + Falsity)))) +;Values$equal1 : +(assert (forall ((a Values$t$type) (b Values$t$type)) (=> (forall ((x Values$elem$type)) + (= (Values$mem x a) + (Values$mem + x b))) (= (Values$eq + a b) + Truth)))) +(define-sort node_set$type () (Array node$type BOOL)) +(declare-fun mk_array_1 () (Array node$type BOOL)) +;mk_array_1_def : +(assert (forall ((mk_array_1_index node$type)) (= (select mk_array_1 + mk_array_1_index) Falsity))) +(define-fun empty_node_set () node_set$type mk_array_1) +(define-sort node_pair_set$type () (Array node$type (Array node$type BOOL))) +(declare-fun mk_array_2 () (Array node$type BOOL)) +;mk_array_2_def : +(assert (forall ((mk_array_2_index node$type)) (= (select mk_array_2 + mk_array_2_index) Falsity))) +(declare-fun mk_array_3 () (Array node$type (Array node$type BOOL))) +;mk_array_3_def : +(assert (forall ((mk_array_3_index node$type)) (= (select mk_array_3 + mk_array_3_index) mk_array_2))) +(define-fun empty_node_pair_set () node_pair_set$type mk_array_3) +(declare-fun mk_array_4 () (Array node$type BOOL)) +;mk_array_4_def : +(assert (forall ((mk_array_4_index node$type)) (= (select mk_array_4 + mk_array_4_index) Truth))) +(declare-fun mk_array_5 () (Array node$type (Array node$type BOOL))) +;mk_array_5_def : +(assert (forall ((mk_array_5_index node$type)) (= (select mk_array_5 + mk_array_5_index) mk_array_4))) +(define-fun full_node_pair_set () node_pair_set$type mk_array_5) +(declare-fun input () (Array node$type value$type)) +(declare-fun t () Int) +;positive_bound : +(assert (> t 0)) +(define-sort message$type () Values$t$type) +(define-sort message_set$type () (Array node$type message$type)) +(define-sort state$type () Values$t$type) +(define-sort state_set$type () (Array node$type state$type)) +(define-fun null_message () message$type Values$empty) +(declare-fun mk_array_6 () (Array node$type message$type)) +;mk_array_6_def : +(assert (forall ((mk_array_6_index node$type)) (= (select mk_array_6 + mk_array_6_index) null_message))) +(define-fun null_message_set () message_set$type mk_array_6) +(define-fun null_state () state$type Values$empty) +(declare-fun mk_array_7 () (Array node$type state$type)) +;mk_array_7_def : +(assert (forall ((mk_array_7_index node$type)) (= (select mk_array_7 + mk_array_7_index) null_state))) +(define-fun null_state_set () state_set$type mk_array_7) +(declare-fun choose (Values$t$type) value$type) +;choosen_value : +(assert (forall ((vals Values$t$type)) (or (= vals Values$empty) (= (Values$mem + (choose + vals) + vals) + Truth)))) +(define-sort failure_pattern$type () node_pair_set$type) +(define-fun is_faulty ((p node$type) (deliver failure_pattern$type)) BOOL +(ite (exists ((q node$type)) (not (= (select (select deliver p) q) Truth))) +Truth Falsity)) +(define-fun is_silent ((p node$type) (deliver failure_pattern$type)) BOOL +(ite (forall ((q node$type)) (not (= (select (select deliver p) q) Truth))) +Truth Falsity)) +(declare-datatypes () ((phase_state$type (init_phase) (send_phase) (recv_phase) (comp_phase)))) +(declare-datatypes () ((clean_state$type (before) (active) (after)))) + +; Var Decls -------------- +(declare-fun init_done () node_set$type) +(declare-fun crashed () Nodes$t$type) +(declare-fun comp_done () node_set$type) +(declare-fun chosen () (Array node$type BOOL)) +(declare-fun recv_done () node_pair_set$type) +(declare-fun phase () phase_state$type) +(declare-fun clean () clean_state$type) +(declare-fun global_state () state_set$type) +(declare-fun messages () (Array node$type message_set$type)) +(declare-fun deliver_message () failure_pattern$type) +(declare-fun crashing () Nodes$t$type) +(declare-fun round () Int) +(declare-fun send_done () node_pair_set$type) + +; Asserts -------------- +(declare-fun mk_array_8 () (Array node$type BOOL)) +;mk_array_8_def : +(assert (forall ((mk_array_8_index node$type)) (= (select mk_array_8 + mk_array_8_index) Falsity))) +(declare-fun mk_array_9 () (Array node$type message_set$type)) +;mk_array_9_def : +(assert (forall ((mk_array_9_index node$type)) (= (select mk_array_9 + mk_array_9_index) null_message_set))) +(assert (not (=> (and (and (and (and (and (and (and (and (and (and (and + (and + (= + clean + before) + (= + global_state + null_state_set)) + (= + messages + mk_array_9)) + (= deliver_message + full_node_pair_set)) + (= comp_done + empty_node_set)) + (= recv_done empty_node_pair_set)) + (= send_done empty_node_pair_set)) + (= init_done empty_node_set)) + (= phase init_phase)) (= crashing + Nodes$empty)) + (= crashed Nodes$empty)) (= round 0)) (= chosen + mk_array_8)) + (forall ((n node$type)) (=> (and (= (select chosen n) Truth) + (= round (+ t 1))) (and (forall + ((n node$type) (m node$type)) + (= (select + (select + send_done + n) + m) + Truth)) + (forall ( + (n node$type) (m node$type)) + (= (select + (select + recv_done + n) m) + Truth)))))))) + +(check-sat) diff --git a/test/regress/regress1/fmf/alg202+1.smt2 b/test/regress/regress1/fmf/alg202+1.smt2 new file mode 100644 index 000000000..ff3460636 --- /dev/null +++ b/test/regress/regress1/fmf/alg202+1.smt2 @@ -0,0 +1,17 @@ +; COMMAND-LINE: --finite-model-find +; EXPECT: unsat +(set-logic ALL) +(declare-sort $$unsorted 0) +(declare-fun sorti1 ($$unsorted) Bool) +(declare-fun op1 ($$unsorted $$unsorted) $$unsorted) +(declare-fun sorti2 ($$unsorted) Bool) +(declare-fun op2 ($$unsorted $$unsorted) $$unsorted) +(declare-fun h ($$unsorted) $$unsorted) +(declare-fun j ($$unsorted) $$unsorted) +(assert (forall ((U $$unsorted) (BOUND_VARIABLE_345 $$unsorted)) (or (not (sorti1 U)) (not (sorti1 BOUND_VARIABLE_345)) (sorti1 (op1 U BOUND_VARIABLE_345))) )) +(assert (forall ((U $$unsorted) (BOUND_VARIABLE_364 $$unsorted)) (or (not (sorti2 U)) (not (sorti2 BOUND_VARIABLE_364)) (sorti2 (op2 U BOUND_VARIABLE_364))) )) +(assert (forall ((U $$unsorted)) (or (not (sorti1 U)) (= U (op1 U U))) )) +(assert (not (forall ((U $$unsorted)) (or (not (sorti2 U)) (= U (op2 U U))) ))) +(assert (not (=> (and (forall ((U $$unsorted)) (or (not (sorti1 U)) (sorti2 (h U))) ) (forall ((V $$unsorted)) (or (not (sorti2 V)) (sorti1 (j V))) )) (not (and (forall ((W $$unsorted) (BOUND_VARIABLE_406 $$unsorted)) (or (not (sorti1 W)) (not (sorti1 BOUND_VARIABLE_406)) (= (op2 (h W) (h BOUND_VARIABLE_406)) (h (op1 W BOUND_VARIABLE_406)))) ) (forall ((Y $$unsorted) (BOUND_VARIABLE_431 $$unsorted)) (or (not (sorti2 Y)) (not (sorti2 BOUND_VARIABLE_431)) (= (op1 (j Y) (j BOUND_VARIABLE_431)) (j (op2 Y BOUND_VARIABLE_431)))) ) (forall ((X1 $$unsorted)) (or (not (sorti2 X1)) (= X1 (h (j X1)))) ) (forall ((X2 $$unsorted)) (or (not (sorti1 X2)) (= X2 (j (h X2)))) )))))) +(assert (and (forall ((U $$unsorted)) (or (not (sorti1 U)) (sorti2 (h U))) ) (forall ((V $$unsorted)) (or (not (sorti2 V)) (sorti1 (j V))) ) (forall ((W $$unsorted) (BOUND_VARIABLE_406 $$unsorted)) (or (not (sorti1 W)) (not (sorti1 BOUND_VARIABLE_406)) (= (op2 (h W) (h BOUND_VARIABLE_406)) (h (op1 W BOUND_VARIABLE_406)))) ) (forall ((Y $$unsorted) (BOUND_VARIABLE_431 $$unsorted)) (or (not (sorti2 Y)) (not (sorti2 BOUND_VARIABLE_431)) (= (op1 (j Y) (j BOUND_VARIABLE_431)) (j (op2 Y BOUND_VARIABLE_431)))) ) (forall ((X1 $$unsorted)) (or (not (sorti2 X1)) (= X1 (h (j X1)))) ) (forall ((X2 $$unsorted)) (or (not (sorti1 X2)) (= X2 (j (h X2)))) ))) +(check-sat) diff --git a/test/regress/regress1/fmf/am-bad-model.cvc b/test/regress/regress1/fmf/am-bad-model.cvc new file mode 100644 index 000000000..e30b5e04a --- /dev/null +++ b/test/regress/regress1/fmf/am-bad-model.cvc @@ -0,0 +1,22 @@ +% EXPECT: sat +OPTION "produce-models"; +OPTION "finite-model-find"; + +f : (BITVECTOR(2),BITVECTOR(2)) ->ARRAY INT OF INT; +f0 : BITVECTOR(2) -> ARRAY INT OF INT; + +td,td1,td2: ARRAY INT OF INT; +ASSERT td1 = td WITH[0]:= 1; +ASSERT td2 = td WITH[0]:= 2; +ASSERT f(0bin01,0bin00)=td1; +ASSERT f(0bin10,0bin00)=td2; +%ASSERT FORALL(i:BITVECTOR(2)) : f0(i)=f(0bin00,i) ; +%Artificial bypass of quantifier for f0 definition +ASSERT f0(0bin00) = f(0bin00,0bin00); +ASSERT f0(0bin01) = f(0bin00,0bin01); +ASSERT f0(0bin10) = f(0bin00,0bin10); +ASSERT f0(0bin11) = f(0bin00,0bin11); +ASSERT FORALL(i:BITVECTOR(2)) : f0(i)=td2 ; + +CHECKSAT; + diff --git a/test/regress/regress1/fmf/bound-int-alt.smt2 b/test/regress/regress1/fmf/bound-int-alt.smt2 new file mode 100644 index 000000000..146487925 --- /dev/null +++ b/test/regress/regress1/fmf/bound-int-alt.smt2 @@ -0,0 +1,18 @@ +; COMMAND-LINE: --fmf-bound-int +; EXPECT: sat +(set-logic UFLIA) +(set-info :status sat) +(declare-sort U 0) +(declare-sort V 0) +(declare-fun P (U Int V Int U Int) Bool) + +(assert (forall ((x U) (y Int) (z V) (w Int) (v U) (d Int)) (=> (and (<= 0 d 1) (<= 2 y 6) (<= 40 w (+ 37 y))) (P x y z w v d)))) + +(declare-fun a () U) +(declare-fun b () V) + +(assert (not (P a 2 b 40 a 0))) +(assert (not (P a 6 b 39 a 0))) +(assert (not (P a 6 b 44 a 0))) + +(check-sat) diff --git a/test/regress/regress1/fmf/bug0909.smt2 b/test/regress/regress1/fmf/bug0909.smt2 new file mode 100644 index 000000000..fc3054c0d --- /dev/null +++ b/test/regress/regress1/fmf/bug0909.smt2 @@ -0,0 +1,54 @@ +; COMMAND-LINE: --finite-model-find --lang=smt2.5 +; EXPECT: unsat +; Preamble -------------- +(set-option :produce-models true) +(set-logic ALL_SUPPORTED) +;(declare-datatypes () ((x2 (x1)))) +(declare-datatypes () ((x5 (x3) (x4)))) +(declare-sort x6 0) +(declare-fun x7 (x6) x5) +(declare-fun x8 () x6) +(assert (not (= x3 (x7 x8)))) +(declare-fun x9 () x6) +(assert (not (= x3 (x7 x9)))) +(declare-fun x11 () Int) +(declare-sort x12 0) +(declare-fun x13 () x12) +(declare-datatypes () ((x17 (x14) (x15) (x16)))) +(declare-datatypes () ((x22 (x21 (x18 Int) (x19 Int) (x20 x5))))) +(declare-datatypes () ((x29 (x28 (x23 x5) (x24 x5) (x25 Int) (x26 Int) (x27 Int))))) +(declare-sort x30 0) +(declare-sort x31 0) +(declare-fun x32 () x31) +(declare-datatypes () ((x36 (x35 (x33 Int) (x34 Int))))) +(declare-fun x37 () x36) +(declare-datatypes () ((x45 (x44 (x38 x5) (x39 x6) (x40 x6) (x41 x6) (x42 x36) (x43 x31))))) +(declare-fun x47 (x12) x31) +(declare-fun x46 (x31) x12) +(declare-datatypes () ((x54 (x49 (x48 x22)) (x51 (x50 x29)) (d53 (s52 x12))))) +(declare-fun x57 (x22) x29) +(declare-fun x56 (x12) x22) +(declare-fun x55 (x29) x22) +(declare-fun x61 () (Array x6 x5)) +(declare-fun x66 () (Array x6 x17)) +(declare-fun x64 () (Array x6 x54)) +(declare-fun x67 () (Array x6 x54)) +(declare-fun x65 () (Array x6 x54)) +(declare-fun x62 () (Array x30 x45)) +(declare-fun x70 () (Array x30 x45)) +(declare-fun x68 () (Array x30 x45)) +(declare-fun x63 () x30) +(declare-fun x59 (x22) x12) +(declare-fun x60 (x29) x12) +(declare-fun x58 (x12) x29) +(declare-fun x71 () x6) +(declare-fun x69 () x6) +(assert +(not + (=> (and + (forall ((x73 x30)) (=> (= x3 (x38 (select x62 x73))) (and (= (select x66 (x40 (select x62 x73))) x15) (= x3 (x7 (x40 (select x62 x73)))) (= (select x61 (x40 (select x62 x73))) x3) (= (x23 (ite (is-x49 (select x67 (x40 (select x62 x73)))) (let ((x74 (x48 (select x67 (x40 (select x62 x73)))))) (x57 x74)) (ite (is-x51 (select x67 (x40 (select x62 x73)))) (let ((x75 (x50 (select x67 (x40 (select x62 x73)))))) x75) (let ((x76 (s52 (select x67 (x40 (select x62 x73)))))) (x58 x76))))) x3)))) + (forall ((x72 x6)) (=> (and (= x16 (select x66 x72)) (= (x7 x72) x3) (= (select x61 x72) x3)) (= (ite (is-d53 (select x67 x72)) x3 x4) x3)))) + + (= (ite (= (x38 (select x62 x63)) x3) (ite (and (=> (= (x40 (select x62 x63)) x69) (=> (= (x41 (select x62 x63)) x71) (=> (= x65 (store x67 x71 (d53 (x46 (x43 (select x62 x63)))))) (=> (= x70 (store x62 x63 (let ((x77 (select x62 x63))) (x44 (x38 x77) (x39 x77) (x40 x77) (x41 x77) (x42 x77) x32)))) (=> (= x68 (store x70 x63 (let ((x78 (select x70 x63))) (x44 x4 (x39 x78) (x40 x78) (x41 x78) (x42 x78) (x43 x78))))) + (=> (= (store x65 x69 (x51 (let ((x82 (ite (is-x49 (select x65 x69)) (let ((x79 (x48 (select x65 x69)))) (x57 x79)) (ite (is-x51 (select x65 x69)) (let ((x80 (x50 (select x65 x69)))) x80) (let ((x81 (s52 (select x65 x69)))) (x58 x81)))))) (x28 x4 x3 (x25 x82) (x26 x82) (+ (x27 (ite (is-x49 (select x65 x69)) (let ((x83 (x48 (select x65 x69)))) (x57 x83)) (ite (is-x51 (select x65 x69)) (let ((x84 (x50 (select x65 x69)))) x84) (let ((x85 (s52 (select x65 x69)))) (x58 x85))))) 1))))) x64) (forall ((x86 x6)) (=> (and (= x3 (x7 x86)) (= x3 (select x61 x86)) (= (select x66 x86) x16)) (= (ite (is-d53 (select x64 x86)) x3 x4) x3))))))))) (= x3 (x38 (select x62 x63)))) x3 x4) (ite (forall ((x87 x6)) (=> (and (= x3 (select x61 x87)) (= x3 (x7 x87)) (= x16 (select x66 x87))) (= x3 (ite (is-d53 (select x67 x87)) x3 x4)))) x3 x4)) x3)))) +(check-sat) diff --git a/test/regress/regress1/fmf/bug651.smt2 b/test/regress/regress1/fmf/bug651.smt2 new file mode 100644 index 000000000..bcfeebd69 --- /dev/null +++ b/test/regress/regress1/fmf/bug651.smt2 @@ -0,0 +1,43 @@ +; COMMAND-LINE: --fmf-fun --no-check-models --lang=smt2.5 +; EXPECT: sat +(set-logic UFDTSLIA) +(set-info :smt-lib-version 2.5) +(set-option :produce-models true) + +(declare-datatypes () ( + (Conditional_Int (Conditional_Int$CAbsent_Int) (Conditional_Int$CPresent_Int (Conditional_Int$CPresent_Int$value Int))) + (Conditional_T_titleType (Conditional_T_titleType$CAbsent_T_titleType) (Conditional_T_titleType$CPresent_T_titleType (Conditional_T_titleType$CPresent_T_titleType$value T_titleType))) + (Conditional_boolean (Conditional_boolean$CAbsent_boolean) (Conditional_boolean$CPresent_boolean (Conditional_boolean$CPresent_boolean$value Bool))) + (Conditional_string (Conditional_string$CAbsent_string) (Conditional_string$CPresent_string (Conditional_string$CPresent_string$value String))) + (Double (Double$CINF) (Double$CNINF) (Double$CNaN) (Double$CValue (Double$CValue$value Int))) + (List_T_titleType (List_T_titleType$CNil_T_titleType) (List_T_titleType$Cstr_T_titleType (List_T_titleType$Cstr_T_titleType$head T_titleType) (List_T_titleType$Cstr_T_titleType$tail List_T_titleType))) + (List_boolean (List_boolean$CNil_boolean) (List_boolean$Cstr_boolean (List_boolean$Cstr_boolean$head Bool) (List_boolean$Cstr_boolean$tail List_boolean))) + (List_string (List_string$CNil_string) (List_string$Cstr_string (List_string$Cstr_string$head String) (List_string$Cstr_string$tail List_string))) + (T_titleType (T_titleType$C_T_titleType (T_titleType$C_T_titleType$base String))) +) ) + +(define-fun f1361$isValid_string((x String)) Bool true) +(define-fun f5131$isValid_T_titleType((x T_titleType)) Bool (and (f1361$isValid_string (T_titleType$C_T_titleType$base x)) (<= (str.len (T_titleType$C_T_titleType$base x)) 80))) +(define-funs-rec + ( + (f5242$isValidElementsList_T_titleType((x List_T_titleType)) Bool) + ) + ( + (=> (is-List_T_titleType$Cstr_T_titleType x) (and (f5131$isValid_T_titleType (List_T_titleType$Cstr_T_titleType$head x)) (f5242$isValidElementsList_T_titleType (List_T_titleType$Cstr_T_titleType$tail x)))) + ) +) +(define-fun f1348$isValid_boolean((x Bool)) Bool true) +(define-funs-rec + ( + (f4169$isValidElementsList_boolean((x List_boolean)) Bool) + ) + ( + (=> (is-List_boolean$Cstr_boolean x) (and (f1348$isValid_boolean (List_boolean$Cstr_boolean$head x)) (f4169$isValidElementsList_boolean (List_boolean$Cstr_boolean$tail x)))) + ) +) + + +(declare-const title T_titleType) +(check-sat) + + diff --git a/test/regress/regress1/fmf/bug723-irrelevant-funs.smt2 b/test/regress/regress1/fmf/bug723-irrelevant-funs.smt2 new file mode 100644 index 000000000..e9b748744 --- /dev/null +++ b/test/regress/regress1/fmf/bug723-irrelevant-funs.smt2 @@ -0,0 +1,52 @@ +; COMMAND-LINE: --fmf-fun-rlv --no-check-models --lang=smt2.5 +; EXPECT: sat +(set-logic ALL_SUPPORTED) +(define-fun $$isTrue$$ ((b Bool)) Bool b) +(define-fun $$isFalse$$ ((b Bool)) Bool (not b)) +(define-fun $$toString$$ ((b Bool)) String (ite b "true" "false") ) +(define-fun $$fromString$$ ((s String)) Bool (= s "true") ) +(define-fun $$inttostr$$ ((i Int)) String (ite (< i 0) (str.++ "-" (int.to.str (- i))) (int.to.str i))) +(declare-fun $$takeWhile$$ (String String) String) +(declare-fun $$takeWhileNot$$ (String String) String) +(declare-fun $$dropWhile$$ (String String) String) +(declare-fun $$dropWhileNot$$ (String String) String) +(declare-datatypes () ( + (AddressType (AddressType$C_AddressType (AddressType$C_AddressType$address String) (AddressType$C_AddressType$city String) (AddressType$C_AddressType$region String) (AddressType$C_AddressType$postalCode String) (AddressType$C_AddressType$country String))) + (Conditional_Int (Conditional_Int$CAbsent_Int) (Conditional_Int$CPresent_Int (Conditional_Int$CPresent_Int$value Int))) + (Conditional_dateTime (Conditional_dateTime$CAbsent_dateTime) (Conditional_dateTime$CPresent_dateTime (Conditional_dateTime$CPresent_dateTime$value Int))) + (Conditional_string (Conditional_string$CAbsent_string) (Conditional_string$CPresent_string (Conditional_string$CPresent_string$value String))) + (CustomerType (CustomerType$C_CustomerType (CustomerType$C_CustomerType$companyName String) (CustomerType$C_CustomerType$contactName String) (CustomerType$C_CustomerType$contactTitle String) (CustomerType$C_CustomerType$phone String) (CustomerType$C_CustomerType$fax Conditional_string) (CustomerType$C_CustomerType$fullAddress AddressType) (CustomerType$C_CustomerType$customerID Int))) + (List_CustomerType (List_CustomerType$CNil_CustomerType) (List_CustomerType$Cstr_CustomerType (List_CustomerType$Cstr_CustomerType$head CustomerType) (List_CustomerType$Cstr_CustomerType$tail List_CustomerType))) + (List_OrderType (List_OrderType$CNil_OrderType) (List_OrderType$Cstr_OrderType (List_OrderType$Cstr_OrderType$head OrderType) (List_OrderType$Cstr_OrderType$tail List_OrderType))) + (OrderType (OrderType$C_OrderType (OrderType$C_OrderType$customerID Int) (OrderType$C_OrderType$employeeID Int) (OrderType$C_OrderType$orderDate Int) (OrderType$C_OrderType$requiredDate Int) (OrderType$C_OrderType$shipInfo ShipInfoType))) + (RootType (RootType$C_RootType (RootType$C_RootType$customers List_CustomerType) (RootType$C_RootType$orders List_OrderType))) + (ShipInfoType (ShipInfoType$C_ShipInfoType (ShipInfoType$C_ShipInfoType$shipVia Int) (ShipInfoType$C_ShipInfoType$freight Int) (ShipInfoType$C_ShipInfoType$shipName String) (ShipInfoType$C_ShipInfoType$shipAddress String) (ShipInfoType$C_ShipInfoType$shipCity String) (ShipInfoType$C_ShipInfoType$shipRegion String) (ShipInfoType$C_ShipInfoType$shipPostalCode String) (ShipInfoType$C_ShipInfoType$shipCountry String) (ShipInfoType$C_ShipInfoType$shippedDate Conditional_dateTime))) +) ) + +(define-fun f2866$toXml((a$$2869 AddressType)) String (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ "<FullAddress>" "<Address>") (AddressType$C_AddressType$address a$$2869)) "</Address>") "<City>") (AddressType$C_AddressType$city a$$2869)) "</City>") "<Region>") (AddressType$C_AddressType$region a$$2869)) "</Region>") "<PostalCode>") (AddressType$C_AddressType$postalCode a$$2869)) "</PostalCode>") "<Country>") (AddressType$C_AddressType$country a$$2869)) "</Country>") "</FullAddress>")) +(define-fun f2656$toXml((c$$2659 CustomerType)) String (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ "<Customer CustomerID=" ($$inttostr$$ (CustomerType$C_CustomerType$customerID c$$2659))) ">") "<CompanyName>") (CustomerType$C_CustomerType$companyName c$$2659)) "</CompanyName>") "<ContactName>") (CustomerType$C_CustomerType$contactName c$$2659)) "</ContactName>") "<ContactTitle>") (CustomerType$C_CustomerType$contactTitle c$$2659)) "</ContactTitle>") "<Phone>") (CustomerType$C_CustomerType$phone c$$2659)) "</Phone>") (ite (is-Conditional_string$CPresent_string (CustomerType$C_CustomerType$fax c$$2659)) (str.++ (str.++ "<Fax>" (Conditional_string$CPresent_string$value (CustomerType$C_CustomerType$fax c$$2659))) "</Fax>") "")) (f2866$toXml (CustomerType$C_CustomerType$fullAddress c$$2659))) "</Customer>")) +(define-funs-rec + ( + (f2574$toXml((lc$$2577 List_CustomerType)) String) + ) + ( + (ite (is-List_CustomerType$CNil_CustomerType lc$$2577) "" (str.++ (f2656$toXml (List_CustomerType$Cstr_CustomerType$head lc$$2577)) (f2574$toXml (List_CustomerType$Cstr_CustomerType$tail lc$$2577)))) + ) +) +(define-fun f2942$toXml((s$$2945 ShipInfoType)) String (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ "<ShipInfo" (ite (is-Conditional_dateTime$CPresent_dateTime (ShipInfoType$C_ShipInfoType$shippedDate s$$2945)) (str.++ (str.++ " ShippedDate=" ($$inttostr$$ (Conditional_dateTime$CPresent_dateTime$value (ShipInfoType$C_ShipInfoType$shippedDate s$$2945)))) ">") ">")) "<ShipVia>") ($$inttostr$$ (ShipInfoType$C_ShipInfoType$shipVia s$$2945))) "</ShipVia>") "<Freight>") ($$inttostr$$ (ShipInfoType$C_ShipInfoType$freight s$$2945))) "</Freight>") "<ShipName>") (ShipInfoType$C_ShipInfoType$shipName s$$2945)) "</ShipName>") "<ShipAddress>") (ShipInfoType$C_ShipInfoType$shipAddress s$$2945)) "</ShipAddress>") "<ShipCity>") (ShipInfoType$C_ShipInfoType$shipCity s$$2945)) "</ShipCity>") "<ShipRegion>") (ShipInfoType$C_ShipInfoType$shipRegion s$$2945)) "</ShipRegion>") "<ShipPostalCode>") (ShipInfoType$C_ShipInfoType$shipPostalCode s$$2945)) "</ShipPostalCode>") "<ShipCountry>") (ShipInfoType$C_ShipInfoType$shipCountry s$$2945)) "</ShipCountry>") "</ShipInfo>")) +(define-fun f2776$toXml((o$$2779 OrderType)) String (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ "<Order>" "<CustomerID>") ($$inttostr$$ (OrderType$C_OrderType$customerID o$$2779))) "</CustomerID>") "<EmployeeID>") ($$inttostr$$ (OrderType$C_OrderType$employeeID o$$2779))) "</EmployeeID>") "<OrderDate>") ($$inttostr$$ (OrderType$C_OrderType$orderDate o$$2779))) "</OrderDate>") "<RequiredDate>") ($$inttostr$$ (OrderType$C_OrderType$requiredDate o$$2779))) "</RequiredDate>") (f2942$toXml (OrderType$C_OrderType$shipInfo o$$2779))) "</Order>")) +(define-funs-rec + ( + (f2615$toXml((lo$$2618 List_OrderType)) String) + ) + ( + (ite (is-List_OrderType$CNil_OrderType lo$$2618) "" (str.++ (f2776$toXml (List_OrderType$Cstr_OrderType$head lo$$2618)) (f2615$toXml (List_OrderType$Cstr_OrderType$tail lo$$2618)))) + ) +) +(define-fun f2526$toXml((r$$2529 RootType)) String (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ "<Root>" "<Customers>") (f2574$toXml (RootType$C_RootType$customers r$$2529))) "</Customers>") "<Orders>") (f2615$toXml (RootType$C_RootType$orders r$$2529))) "</Orders>") "</Root>")) + +(declare-fun $Report$3105$0$1$() String) +(assert (= $Report$3105$0$1$ "<Root><Customers></Customers><Orders></Orders></Root>")) +; should be fast since functions introduced by define-fun-rec do not appear in the ground assertion +(check-sat) + diff --git a/test/regress/regress1/fmf/bug764.smt2 b/test/regress/regress1/fmf/bug764.smt2 new file mode 100644 index 000000000..3172fd695 --- /dev/null +++ b/test/regress/regress1/fmf/bug764.smt2 @@ -0,0 +1,28 @@ +; COMMAND-LINE: --fmf-fun --no-check-models --lang=smt2.5 +; EXPECT: sat +(set-logic ALL) +(set-info :status sat) + +(define-fun BoolToString ((b Bool)) String (ite b "true" "false") ) + +(declare-datatypes () ( + (Color (red) (white) (blue)) +) ) + +(define-fun ColorToString ((c Color)) String (ite (is-red c) "red" (ite (is-white c) "white" "blue")) ) + +(declare-datatypes () ( + (CP (cp (b Bool) (c Color))) +) ) + +(define-fun-rec CPToString ((cp CP)) String (str.++ "cp(" (BoolToString (b cp)) "," (ColorToString (c cp)) ")")) + +(declare-fun CPFromString (String) CP) + +(assert (forall ((cp1 CP)) (= cp1 (CPFromString (CPToString cp1))))) + +(declare-fun cpx() CP) +(assert (= cpx (CPFromString "cp(true,white)"))) + +(check-sat) + diff --git a/test/regress/regress1/fmf/cons-sets-bounds.smt2 b/test/regress/regress1/fmf/cons-sets-bounds.smt2 new file mode 100644 index 000000000..5e3c2952b --- /dev/null +++ b/test/regress/regress1/fmf/cons-sets-bounds.smt2 @@ -0,0 +1,26 @@ +; COMMAND-LINE: --fmf-bound +; EXPECT: sat +(set-logic ALL) +(declare-datatypes ((list 0)) (((cons (head Int) (tail list)) (nil)))) + +(declare-fun P (Int) Bool) +(declare-fun S () (Set list)) + +; can use simple unification to infer bounds on x and y +(assert (forall ((x Int) (y list)) (=> (member (cons x y) S) (P x)))) + +(assert (member (cons 4 (cons 1 nil)) S)) +(assert (member (cons 2 nil) S)) + +; should construct instantiation involving selectors for l +(declare-fun l () list) +(assert ((_ is cons) l)) +(assert (member l S)) + +; should not contribute to instantiations +(assert (member nil S)) + +(assert (not (P 1))) +(assert (not (P 0))) + +(check-sat) diff --git a/test/regress/regress1/fmf/constr-ground-to.smt2 b/test/regress/regress1/fmf/constr-ground-to.smt2 new file mode 100644 index 000000000..bc6d9e948 --- /dev/null +++ b/test/regress/regress1/fmf/constr-ground-to.smt2 @@ -0,0 +1,43 @@ +; COMMAND-LINE: --fmf-fun --lang=smt2.5 +; EXPECT: sat +(set-logic UFDTLIA) +(declare-datatypes () ( + ( + Term + (str (sv IntList)) + ) + ( + IntList + (sn) + (sc (sh Int) (st IntList)) + ) +)) +(declare-const t Term) +(assert ( + and + (is-str t) + (is-sc (sv t)) + (is-sc (st (sv t))) + (is-sc (st (st (sv t)))) + (is-sc (st (st (st (sv t))))) + (is-sc (st (st (st (st (sv t)))))) + (is-sc (st (st (st (st (st (sv t))))))) + (is-sc (st (st (st (st (st (st (sv t)))))))) + (is-sc (st (st (st (st (st (st (st (sv t))))))))) + (is-sc (st (st (st (st (st (st (st (st (sv t)))))))))) + (is-sc (st (st (st (st (st (st (st (st (st (sv t))))))))))) + (is-sc (st (st (st (st (st (st (st (st (st (st (sv t)))))))))))) + (is-sc (st (st (st (st (st (st (st (st (st (st (st (sv t))))))))))))) + (is-sc (st (st (st (st (st (st (st (st (st (st (st (st (sv t)))))))))))))) + (is-sc (st (st (st (st (st (st (st (st (st (st (st (st (st (sv t))))))))))))))) + (is-sc (st (st (st (st (st (st (st (st (st (st (st (st (st (st (sv t)))))))))))))))) + (is-sc (st (st (st (st (st (st (st (st (st (st (st (st (st (st (st (sv t))))))))))))))))) + (is-sc (st (st (st (st (st (st (st (st (st (st (st (st (st (st (st (st (sv t)))))))))))))))))) + (is-sc (st (st (st (st (st (st (st (st (st (st (st (st (st (st (st (st (st (sv t))))))))))))))))))) + (is-sc (st (st (st (st (st (st (st (st (st (st (st (st (st (st (st (st (st (st (sv t)))))))))))))))))))) + (is-sc (st (st (st (st (st (st (st (st (st (st (st (st (st (st (st (st (st (st (st (sv t))))))))))))))))))))) + (is-sc (st (st (st (st (st (st (st (st (st (st (st (st (st (st (st (st (st (st (st (st (sv t)))))))))))))))))))))) + (is-sc (st (st (st (st (st (st (st (st (st (st (st (st (st (st (st (st (st (st (st (st (st (sv t))))))))))))))))))))))) + (is-sc (st (st (st (st (st (st (st (st (st (st (st (st (st (st (st (st (st (st (st (st (st (st (sv t)))))))))))))))))))))))) +)) +(check-sat) diff --git a/test/regress/regress1/fmf/datatypes-ufinite-nested.smt2 b/test/regress/regress1/fmf/datatypes-ufinite-nested.smt2 new file mode 100644 index 000000000..6b30907ae --- /dev/null +++ b/test/regress/regress1/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 0) (ufin2 0)) (((cons1 (s11 U) (s13 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/regress1/fmf/datatypes-ufinite.smt2 b/test/regress/regress1/fmf/datatypes-ufinite.smt2 new file mode 100644 index 000000000..a19c8f027 --- /dev/null +++ b/test/regress/regress1/fmf/datatypes-ufinite.smt2 @@ -0,0 +1,17 @@ +; COMMAND-LINE: --finite-model-find --lang=smt2.5 +; 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/regress1/fmf/dt-proper-model.smt2 b/test/regress/regress1/fmf/dt-proper-model.smt2 new file mode 100644 index 000000000..0e66db996 --- /dev/null +++ b/test/regress/regress1/fmf/dt-proper-model.smt2 @@ -0,0 +1,16 @@ +; COMMAND-LINE: --finite-model-find +; EXPECT: sat +(set-logic ALL_SUPPORTED) +(set-info :status sat) +(declare-sort U 0) +(declare-datatypes ((D 0)) (((cons (x Int) (y U))))) +(declare-fun d1 () D) +(declare-fun d2 () D) +(declare-fun d3 () D) +(declare-fun d4 () D) +(assert (distinct d1 d2 d3 d4)) +(assert (forall ((x U) (y U)) (= x y))) +(declare-fun a () U) +(declare-fun P (U) Bool) +(assert (P a)) +(check-sat) diff --git a/test/regress/regress1/fmf/fc-pigeonhole19.smt2 b/test/regress/regress1/fmf/fc-pigeonhole19.smt2 new file mode 100644 index 000000000..f145013d8 --- /dev/null +++ b/test/regress/regress1/fmf/fc-pigeonhole19.smt2 @@ -0,0 +1,20 @@ +(set-logic UFC) +(set-info :status unsat) + +(declare-sort P 0) +(declare-sort H 0) + +(declare-fun p () P) +(declare-fun h () H) + +; pigeonhole using native cardinality constraints +(assert (fmf.card p 19)) +(assert (not (fmf.card p 18))) +(assert (fmf.card h 18)) +(assert (not (fmf.card h 17))) + +; each pigeon has different holes +(declare-fun f (P) H) +(assert (forall ((p1 P) (p2 P)) (=> (not (= p1 p2)) (not (= (f p1) (f p2)))))) + +(check-sat)
\ No newline at end of file diff --git a/test/regress/regress1/fmf/fib-core.smt2 b/test/regress/regress1/fmf/fib-core.smt2 new file mode 100644 index 000000000..e00f19ad4 --- /dev/null +++ b/test/regress/regress1/fmf/fib-core.smt2 @@ -0,0 +1,19 @@ +; COMMAND-LINE: --finite-model-find --fmf-inst-engine +; EXPECT: unsat +(set-logic ALL_SUPPORTED) +(set-info :status unsat) +(declare-sort I_fb 0) +(declare-fun fb_arg_0_1 (I_fb) Int) +(declare-fun fb (Int) Int) + +(assert (forall ((?j I_fb)) (= (fb (fb_arg_0_1 ?j)) (ite (not (>= (fb_arg_0_1 ?j) 2)) (fb_arg_0_1 ?j) (+ (fb (+ (- 1) (fb_arg_0_1 ?j))) (fb (+ (- 2) (fb_arg_0_1 ?j)))))) ) ) + +(assert (forall ((?i I_fb)) (ite (not (>= (fb_arg_0_1 ?i) 2)) true (and (not (forall ((?z I_fb)) (not (= (fb_arg_0_1 ?i) (+ 1 (fb_arg_0_1 ?z)))) )) (not (forall ((?z I_fb)) (not (= (fb_arg_0_1 ?i) (+ 2 (fb_arg_0_1 ?z)))) )))) ) ) + +(assert (forall ((?i I_fb)) (or (>= (fb_arg_0_1 ?i) 2) (and (not (>= (fb_arg_0_1 ?i) 2)) (not (forall ((?z I_fb)) (not (= (fb_arg_0_1 ?i) (+ 1 (fb_arg_0_1 ?z)))) )) (not (forall ((?z I_fb)) (not (= (fb_arg_0_1 ?i) (+ 2 (fb_arg_0_1 ?z)))) )))) )) + + +(assert (not (= (fb 5) 5)) ) +(assert (not (forall ((?z I_fb)) (not (= (fb_arg_0_1 ?z) 5)) ))) + +(check-sat)
\ No newline at end of file diff --git a/test/regress/regress1/fmf/fmf-bound-2dim.smt2 b/test/regress/regress1/fmf/fmf-bound-2dim.smt2 new file mode 100644 index 000000000..5f5c22770 --- /dev/null +++ b/test/regress/regress1/fmf/fmf-bound-2dim.smt2 @@ -0,0 +1,15 @@ +; COMMAND-LINE: --fmf-bound +; EXPECT: sat +(set-logic ALL) +(set-info :status sat) +(declare-fun P (Int Int) Bool) + +(declare-fun a () Int) +(assert (> a 10)) + +(assert (forall ((x Int) (y Int)) +(=> (and (<= a x) (<= x (+ a 5)) (<= 14 y) (<= y (+ 7 x))) +(P x y)))) +(assert (not (P 15 4))) + +(check-sat) diff --git a/test/regress/regress1/fmf/fmf-bound-int.smt2 b/test/regress/regress1/fmf/fmf-bound-int.smt2 new file mode 100644 index 000000000..fb3106bdf --- /dev/null +++ b/test/regress/regress1/fmf/fmf-bound-int.smt2 @@ -0,0 +1,7 @@ +; COMMAND-LINE: --finite-model-find --fmf-bound-int +; EXPECT: sat +(set-logic UFLIA) +(declare-fun P (Int Int) Bool) +(declare-fun Q (Int) Bool) +(assert (forall ((x Int)) (=> (and (<= 0 x) (<= x (ite (P 0 0) 10 20))) (Q x)))) +(check-sat) diff --git a/test/regress/regress1/fmf/fmf-fun-no-elim-ext-arith.smt2 b/test/regress/regress1/fmf/fmf-fun-no-elim-ext-arith.smt2 new file mode 100644 index 000000000..0618e28cb --- /dev/null +++ b/test/regress/regress1/fmf/fmf-fun-no-elim-ext-arith.smt2 @@ -0,0 +1,18 @@ +; COMMAND-LINE: --fmf-fun --no-check-models --rewrite-divk +; EXPECT: sat +(set-logic UFLIA) +(set-info :status sat) +(define-fun-rec int-and ((n Int) (n1 Int) (n2 Int)) Bool ( + or + (= n1 n 0) + (= n2 n 0) + ( + and + (> n1 0) + (> n2 0) + (>= n 0) + (= (not (= (mod n 2 ) 0)) (and (not (= (mod n1 2 ) 0)) (not (= (mod n2 2) 0)))) + (int-and (div n 2) (div n1 2) (div n2 2)) + ) +)) +(check-sat) diff --git a/test/regress/regress1/fmf/fmf-fun-no-elim-ext-arith2.smt2 b/test/regress/regress1/fmf/fmf-fun-no-elim-ext-arith2.smt2 new file mode 100644 index 000000000..07f1e6674 --- /dev/null +++ b/test/regress/regress1/fmf/fmf-fun-no-elim-ext-arith2.smt2 @@ -0,0 +1,25 @@ +; COMMAND-LINE: --fmf-fun --no-check-models --rewrite-divk +; EXPECT: sat +(set-logic UFLIA) +(set-info :status sat) +(define-fun-rec int-and ((n Int) (n1 Int) (n2 Int)) Bool ( + or + (= n1 n 0) + (= n2 n 0) + ( + and + (> n1 0) + (> n2 0) + (>= n 0) + (= (not (= (mod n 2 ) 0)) (and (not (= (mod n1 2 ) 0)) (not (= (mod n2 2) 0)))) + (int-and (div n 2) (div n1 2) (div n2 2)) + ) +)) +(declare-const x Int) +(declare-const y Int) +(declare-const z Int) +(assert (= x 1)) +(assert (= y 1)) +(assert (= z 1)) +(assert (int-and z x y)) +(check-sat) diff --git a/test/regress/regress1/fmf/fmf-strange-bounds.smt2 b/test/regress/regress1/fmf/fmf-strange-bounds.smt2 new file mode 100644 index 000000000..7812c2431 --- /dev/null +++ b/test/regress/regress1/fmf/fmf-strange-bounds.smt2 @@ -0,0 +1,35 @@ +; COMMAND-LINE: --fmf-bound +; EXPECT: sat +(set-logic ALL) +(set-info :status sat) +(declare-sort U 0) +(declare-fun P (Int Int U) Bool) + +(declare-fun S () (Set Int)) + +(declare-fun f (Int) U) +(declare-fun g (Int) U) + +(declare-fun h (U) Int) + +(assert (member 77 S)) +(assert (>= (h (f 77)) 3)) +(assert (>= (h (g 77)) 2)) +(assert (not (= (g 77) (f 77)))) + +(assert (forall ((x Int) (y Int) (z U)) (=> +(or (= z (f x)) (= z (g x))) +(=> (member x S) +(=> (and (<= 0 y) (<= y (h z))) +(P x y z)))))) + + +(declare-fun Q (U Int) Bool) +(declare-const a U) +(declare-const b U) +(declare-const c U) +(assert (distinct a b c)) +(assert (forall ((x U) (y Int)) (=> (and (<= 3 y) (<= y 10) (or (= x c) (= x (f y)))) (Q x y)))) +(assert (not (Q b 6))) + +(check-sat) diff --git a/test/regress/regress1/fmf/forall_unit_data.smt2 b/test/regress/regress1/fmf/forall_unit_data.smt2 new file mode 100644 index 000000000..6971c4d0a --- /dev/null +++ b/test/regress/regress1/fmf/forall_unit_data.smt2 @@ -0,0 +1,10 @@ +; COMMAND-LINE: --finite-model-find --lang=smt2.5 +; 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/regress1/fmf/fore19-exp2-core.smt2 b/test/regress/regress1/fmf/fore19-exp2-core.smt2 new file mode 100644 index 000000000..4b4d57af3 --- /dev/null +++ b/test/regress/regress1/fmf/fore19-exp2-core.smt2 @@ -0,0 +1,72 @@ +; COMMAND-LINE: --lang=smt2.5 +; EXPECT: unsat +(set-logic ALL_SUPPORTED) +(set-info :status unsat) +(declare-datatypes () ((St (Block!2236 (body!2237 List!2293)) (For!2238 (init!2239 St) (expr!2240 Ex) (step!2241 St) (body!2242 St)) (IfTE (expr!2244 Ex) (then!2245 St) (elze!2246 St)) (Skip!2250) (While (expr!2252 Ex) (body St))) +(Ex (Var!2291 (varID!2292 (_ BitVec 32)))) +(List!2293 (Cons!2294 (head!2295 St) (tail!2296 List!2293)) (Nil!2297)) +)) +(declare-fun error_value!2298 () Bool) +(declare-fun error_value!2299 () List!2293) +(declare-fun s () St) +(declare-fun body!2242_uf_1 (St) St) +(declare-fun step!2241_uf_2 (St) St) +(declare-fun init!2239_uf_3 (St) St) +(declare-fun elze!2246_uf_4 (St) St) +(declare-fun then!2245_uf_5 (St) St) +(declare-fun body!2237_uf_6 (St) List!2293) +(declare-fun tail!2296_uf_7 (List!2293) List!2293) +(declare-fun head!2295_uf_8 (List!2293) St) +(declare-fun expr!2240_uf_9 (St) Ex) +(declare-fun body_uf_10 (St) St) +(declare-fun expr!2252_uf_11 (St) Ex) +(declare-fun expr!2244_uf_12 (St) Ex) +(declare-fun iwf (St) Bool) +(declare-fun iwfl (List!2293) Bool) +(declare-fun ewl (St) St) +(declare-fun ewlList!211 (List!2293) List!2293) +(declare-sort I_iwf 0) +(declare-fun iwf_arg_0_13 (I_iwf) St) +(declare-sort I_iwfl 0) +(declare-fun iwfl_arg_0_14 (I_iwfl) List!2293) +(declare-sort I_ewl 0) +(declare-fun ewl_arg_0_15 (I_ewl) St) +(declare-sort I_ewlList!211 0) +(declare-fun ewlList!211_arg_0_16 (I_ewlList!211) List!2293) +(declare-fun termITE_17 () St) +(declare-fun termITE_18 () St) +(declare-fun termITE_19 () St) +(declare-fun termITE_20 () St) + +(assert +(and +(forall ((?i1 I_ewl)) (= (ewl (ewl_arg_0_15 ?i1)) + +(ite (is-IfTE (ewl_arg_0_15 ?i1)) (IfTE (ite (is-IfTE (ewl_arg_0_15 ?i1)) (expr!2244 (ewl_arg_0_15 ?i1)) (expr!2244_uf_12 (ewl_arg_0_15 ?i1))) (ewl (ite (is-IfTE (ewl_arg_0_15 ?i1)) (then!2245 (ewl_arg_0_15 ?i1)) (then!2245_uf_5 (ewl_arg_0_15 ?i1)))) (ewl (ite (is-IfTE (ewl_arg_0_15 ?i1)) (elze!2246 (ewl_arg_0_15 ?i1)) (elze!2246_uf_4 (ewl_arg_0_15 ?i1))))) + +(ite (is-While (ewl_arg_0_15 ?i1)) (For!2238 Skip!2250 (ite (is-While (ewl_arg_0_15 ?i1)) (expr!2252 (ewl_arg_0_15 ?i1)) (expr!2252_uf_11 (ewl_arg_0_15 ?i1))) Skip!2250 (ewl (ite (is-While (ewl_arg_0_15 ?i1)) (body (ewl_arg_0_15 ?i1)) (body_uf_10 (ewl_arg_0_15 ?i1))))) + +(ite (is-For!2238 (ewl_arg_0_15 ?i1)) (For!2238 (ewl (ite (is-For!2238 (ewl_arg_0_15 ?i1)) (init!2239 (ewl_arg_0_15 ?i1)) (init!2239_uf_3 (ewl_arg_0_15 ?i1)))) (ite (is-For!2238 (ewl_arg_0_15 ?i1)) (expr!2240 (ewl_arg_0_15 ?i1)) (expr!2240_uf_9 (ewl_arg_0_15 ?i1))) (ewl (ite (is-For!2238 (ewl_arg_0_15 ?i1)) (step!2241 (ewl_arg_0_15 ?i1)) (step!2241_uf_2 (ewl_arg_0_15 ?i1)))) (ewl (ite (is-For!2238 (ewl_arg_0_15 ?i1)) (body!2242 (ewl_arg_0_15 ?i1)) (body!2242_uf_1 (ewl_arg_0_15 ?i1))))) + +(ewl_arg_0_15 ?i1))))) ) + + +(forall ((?i2 I_ewl)) (ite (is-IfTE (ewl_arg_0_15 ?i2)) (and (not (forall ((?z I_ewl)) (not (= (ewl_arg_0_15 ?z) (ite (is-IfTE (ewl_arg_0_15 ?i2)) (then!2245 (ewl_arg_0_15 ?i2)) (then!2245_uf_5 (ewl_arg_0_15 ?i2))))) )) (not (forall ((?z I_ewl)) (not (= (ewl_arg_0_15 ?z) (ite (is-IfTE (ewl_arg_0_15 ?i2)) (elze!2246 (ewl_arg_0_15 ?i2)) (elze!2246_uf_4 (ewl_arg_0_15 ?i2))))) ))) (ite (is-While (ewl_arg_0_15 ?i2)) (not (forall ((?z I_ewl)) (not (= (ewl_arg_0_15 ?z) (ite (is-While (ewl_arg_0_15 ?i2)) (body (ewl_arg_0_15 ?i2)) (body_uf_10 (ewl_arg_0_15 ?i2))))) )) (ite (is-For!2238 (ewl_arg_0_15 ?i2)) (and (not (forall ((?z I_ewl)) (not (= (ewl_arg_0_15 ?z) (ite (is-For!2238 (ewl_arg_0_15 ?i2)) (init!2239 (ewl_arg_0_15 ?i2)) (init!2239_uf_3 (ewl_arg_0_15 ?i2))))) )) (not (forall ((?z I_ewl)) (not (= (ewl_arg_0_15 ?z) (ite (is-For!2238 (ewl_arg_0_15 ?i2)) (step!2241 (ewl_arg_0_15 ?i2)) (step!2241_uf_2 (ewl_arg_0_15 ?i2))))) )) (not (forall ((?z I_ewl)) (not (= (ewl_arg_0_15 ?z) (ite (is-For!2238 (ewl_arg_0_15 ?i2)) (body!2242 (ewl_arg_0_15 ?i2)) (body!2242_uf_1 (ewl_arg_0_15 ?i2))))) ))) true))) ) +(forall ((?i3 I_iwf)) (= (iwf (iwf_arg_0_13 ?i3)) (ite (is-Block!2236 (iwf_arg_0_13 ?i3)) (iwfl (ite (is-Block!2236 (iwf_arg_0_13 ?i3)) (body!2237 (iwf_arg_0_13 ?i3)) (body!2237_uf_6 (iwf_arg_0_13 ?i3)))) (ite (is-IfTE (iwf_arg_0_13 ?i3)) (and (iwf (ite (is-IfTE (iwf_arg_0_13 ?i3)) (elze!2246 (iwf_arg_0_13 ?i3)) (elze!2246_uf_4 (iwf_arg_0_13 ?i3)))) (iwf (ite (is-IfTE (iwf_arg_0_13 ?i3)) (then!2245 (iwf_arg_0_13 ?i3)) (then!2245_uf_5 (iwf_arg_0_13 ?i3))))) (ite (is-While (iwf_arg_0_13 ?i3)) false (ite (is-For!2238 (iwf_arg_0_13 ?i3)) (and (iwf (ite (is-For!2238 (iwf_arg_0_13 ?i3)) (body!2242 (iwf_arg_0_13 ?i3)) (body!2242_uf_1 (iwf_arg_0_13 ?i3)))) (iwf (ite (is-For!2238 (iwf_arg_0_13 ?i3)) (step!2241 (iwf_arg_0_13 ?i3)) (step!2241_uf_2 (iwf_arg_0_13 ?i3)))) (iwf (ite (is-For!2238 (iwf_arg_0_13 ?i3)) (init!2239 (iwf_arg_0_13 ?i3)) (init!2239_uf_3 (iwf_arg_0_13 ?i3))))) true))))) ) +(forall ((?i4 I_iwf)) (ite (is-Block!2236 (iwf_arg_0_13 ?i4)) (not (forall ((?z I_iwfl)) (not (= (iwfl_arg_0_14 ?z) (ite (is-Block!2236 (iwf_arg_0_13 ?i4)) (body!2237 (iwf_arg_0_13 ?i4)) (body!2237_uf_6 (iwf_arg_0_13 ?i4))))) )) (ite (is-IfTE (iwf_arg_0_13 ?i4)) (and (not (forall ((?z I_iwf)) (not (= (iwf_arg_0_13 ?z) (ite (is-IfTE (iwf_arg_0_13 ?i4)) (elze!2246 (iwf_arg_0_13 ?i4)) (elze!2246_uf_4 (iwf_arg_0_13 ?i4))))) )) (not (forall ((?z I_iwf)) (not (= (iwf_arg_0_13 ?z) (ite (is-IfTE (iwf_arg_0_13 ?i4)) (then!2245 (iwf_arg_0_13 ?i4)) (then!2245_uf_5 (iwf_arg_0_13 ?i4))))) ))) (ite (is-While (iwf_arg_0_13 ?i4)) true (ite (is-For!2238 (iwf_arg_0_13 ?i4)) (and (not (forall ((?z I_iwf)) (not (= (iwf_arg_0_13 ?z) (ite (is-For!2238 (iwf_arg_0_13 ?i4)) (body!2242 (iwf_arg_0_13 ?i4)) (body!2242_uf_1 (iwf_arg_0_13 ?i4))))) )) (not (forall ((?z I_iwf)) (not (= (iwf_arg_0_13 ?z) (ite (is-For!2238 (iwf_arg_0_13 ?i4)) (step!2241 (iwf_arg_0_13 ?i4)) (step!2241_uf_2 (iwf_arg_0_13 ?i4))))) )) (not (forall ((?z I_iwf)) (not (= (iwf_arg_0_13 ?z) (ite (is-For!2238 (iwf_arg_0_13 ?i4)) (init!2239 (iwf_arg_0_13 ?i4)) (init!2239_uf_3 (iwf_arg_0_13 ?i4))))) ))) true)))) ) +(is-IfTE s) +(iwf s) +(not (forall ((?z I_iwf)) (not (= (iwf_arg_0_13 ?z) s)) )) +(ite (is-IfTE s) (= termITE_17 (then!2245 s)) (= termITE_17 (then!2245_uf_5 s))) +(ite (is-IfTE s) (= termITE_18 (then!2245 s)) (= termITE_18 (then!2245_uf_5 s))) +(=> (and (iwf termITE_17) (not (forall ((?z I_iwf)) (not (= (iwf_arg_0_13 ?z) termITE_18)) ))) (and (= (ewl termITE_17) termITE_17) (not (forall ((?z I_ewl)) (not (= (ewl_arg_0_15 ?z) termITE_18)) )))) +(ite (is-IfTE s) (= termITE_19 (elze!2246 s)) (= termITE_19 (elze!2246_uf_4 s))) +(ite (is-IfTE s) (= termITE_20 (elze!2246 s)) (= termITE_20 (elze!2246_uf_4 s))) +(=> (and (iwf termITE_19) (not (forall ((?z I_iwf)) (not (= (iwf_arg_0_13 ?z) termITE_20)) ))) (and (= (ewl termITE_19) termITE_19) (not (forall ((?z I_ewl)) (not (= (ewl_arg_0_15 ?z) termITE_20)) )))) +(not (= (ewl s) s)) +(not (forall ((?z I_ewl)) (not (= (ewl_arg_0_15 ?z) s)) )) + + +) +) +(check-sat) diff --git a/test/regress/regress1/fmf/german169.smt2 b/test/regress/regress1/fmf/german169.smt2 new file mode 100644 index 000000000..c88de064c --- /dev/null +++ b/test/regress/regress1/fmf/german169.smt2 @@ -0,0 +1,103 @@ +; COMMAND-LINE: --finite-model-find --lang=smt2.5 +; EXPECT: sat +(set-logic ALL_SUPPORTED) +(set-info :status sat) +(declare-datatypes () ((UNIT (Unit)))) +(declare-datatypes () ((BOOL (Truth) (Falsity)))) + +; Decls -------------- +(declare-sort node$type 0) +(declare-sort data$type 0) +(declare-datatypes () ((cache_state$type (invalid) (shared) (exclusive)))) +(declare-datatypes () ((cache$type (c_cache$type (c_state cache_state$type) (c_data data$type))))) +(declare-datatypes () ((msg_cmd$type (empty) (reqs) (reqe) (inv) (invack) (gnts) (gnte)))) +(declare-datatypes () ((msg$type (c_msg$type (m_cmd msg_cmd$type) (m_data data$type))))) +(declare-fun dummy () data$type) + +; Var Decls -------------- +(declare-fun memdata$1 () data$type) +(declare-fun shrset$1 () (Array node$type BOOL)) +(declare-fun recv_invack$i () node$type) +(declare-fun exgntd () BOOL) +(declare-fun chan3$1 () (Array node$type msg$type)) +(declare-fun shrset () (Array node$type BOOL)) +(declare-fun exgntd$1 () BOOL) +(declare-fun chan2 () (Array node$type msg$type)) +(declare-fun chan3 () (Array node$type msg$type)) +(declare-fun auxnode () node$type) +(declare-fun curcmd () msg_cmd$type) + +; Asserts -------------- +(assert (not (=> (and (and (forall ((n node$type)) + (=> (= (m_cmd (select + chan2 + n)) + gnte) (= exgntd + Truth))) + (forall ((n node$type)) + (=> (= exgntd Truth) + (= (select shrset n) + (ite (= n auxnode) Truth + Falsity))))) (forall + ((n node$type)) + (=> (= + (m_cmd + (select + chan3 + n)) + invack) + (= (m_cmd + (select + chan2 + n)) + empty)))) + (=> (= (m_cmd (select chan3 recv_invack$i)) + invack) (=> (not (= curcmd empty)) + (=> (= chan3$1 (store + chan3 + recv_invack$i + (let ( + (vup_228 + (select + chan3 + recv_invack$i))) + (c_msg$type + empty + (m_data + vup_228))))) + (=> (= shrset$1 (store + shrset + recv_invack$i + Falsity)) + (= (ite (= exgntd Truth) + (ite (=> (= exgntd$1 + Falsity) + (=> (= memdata$1 + (m_data + (select + chan3$1 + recv_invack$i))) + (forall ( + (n node$type)) + (=> (= (m_cmd + (select + chan2 + n)) + gnte) + (= exgntd$1 + Truth))))) + Truth Falsity) + (ite (forall ( + (n node$type)) + (=> (= (m_cmd + (select + chan2 + n)) + gnte) + (= exgntd + Truth))) + Truth Falsity)) + Truth)))))))) + +(check-sat) +(exit) diff --git a/test/regress/regress1/fmf/german73.smt2 b/test/regress/regress1/fmf/german73.smt2 new file mode 100644 index 000000000..64f551d55 --- /dev/null +++ b/test/regress/regress1/fmf/german73.smt2 @@ -0,0 +1,105 @@ +; COMMAND-LINE: --finite-model-find --lang=smt2.5 +; EXPECT: unsat +(set-logic ALL_SUPPORTED) +(set-info :status unsat) +(declare-datatypes () ((UNIT (Unit)))) +(declare-datatypes () ((BOOL (Truth) (Falsity)))) + +; Decls -------------- +(declare-sort node$type 0) +(declare-sort data$type 0) +(declare-datatypes () ((cache_state$type (invalid) (shared) (exclusive)))) +(declare-datatypes () ((cache$type (c_cache$type (c_state cache_state$type) (c_data data$type))))) +(declare-datatypes () ((msg_cmd$type (empty) (reqs) (reqe) (inv) (invack) (gnts) (gnte)))) +(declare-datatypes () ((msg$type (c_msg$type (m_cmd msg_cmd$type) (m_data data$type))))) +(declare-fun dummy () data$type) + +; Var Decls -------------- +(declare-fun memdata$1 () data$type) +(declare-fun shrset$1 () (Array node$type BOOL)) +(declare-fun recv_invack$i () node$type) +(declare-fun exgntd () BOOL) +(declare-fun invset () (Array node$type BOOL)) +(declare-fun chan3$1 () (Array node$type msg$type)) +(declare-fun shrset () (Array node$type BOOL)) +(declare-fun exgntd$1 () BOOL) +(declare-fun chan2 () (Array node$type msg$type)) +(declare-fun chan3 () (Array node$type msg$type)) +(declare-fun curcmd () msg_cmd$type) + +; Asserts -------------- +(assert (not (=> (and (forall ((n node$type)) + (=> (= (select invset n) + Truth) (= (select + shrset + n) Truth))) + (forall ((n node$type)) (=> + (or + (= + (m_cmd + (select + chan2 + n)) + inv) + (= + (m_cmd + (select + chan3 + n)) + invack)) + (not + (= + (select + invset + n) + Truth))))) + (=> (= (m_cmd (select chan3 recv_invack$i)) + invack) (=> (not (= curcmd empty)) + (=> (= chan3$1 (store + chan3 + recv_invack$i + (let ( + (vup_101 + (select + chan3 + recv_invack$i))) + (c_msg$type + empty + (m_data + vup_101))))) + (=> (= shrset$1 (store + shrset + recv_invack$i + Falsity)) + (= (ite (= exgntd Truth) + (ite (=> (= exgntd$1 + Falsity) + (=> (= memdata$1 + (m_data + (select + chan3$1 + recv_invack$i))) + (forall ( + (n node$type)) + (=> (= (select + invset + n) + Truth) + (= (select + shrset$1 + n) Truth))))) + Truth Falsity) + (ite (forall ( + (n node$type)) + (=> (= (select + invset + n) + Truth) + (= (select + shrset$1 + n) Truth))) + Truth Falsity)) + Truth)))))))) + +(check-sat) +(exit) diff --git a/test/regress/regress1/fmf/issue916-fmf-or.smt2 b/test/regress/regress1/fmf/issue916-fmf-or.smt2 new file mode 100644 index 000000000..0c51e39af --- /dev/null +++ b/test/regress/regress1/fmf/issue916-fmf-or.smt2 @@ -0,0 +1,48 @@ +; COMMAND-LINE: --fmf-fun --no-check-models +; EXPECT: sat + +(set-logic UFDTLIA) +(set-info :smt-lib-version 2.5) + +(define-funs-rec + ( + (validIdValue ((x Int)(v Int)) Bool) + ) + ( + (or + (and (= x 0) (< (- 10) v 10) ) + (and (= x 1) (<= (- 100) v (- 10)) ) + (and (= x 2) (<= 10 v 100) ) + (and (= x 3) (< (- 1000) v (- 100)) ) + (and (= x 4) (< 100 v 1000) ) + (and (= x 5) (<= (- 1000) v) ) + (and (= x 6) (<= v 1000) ) + (validIdValue (- x 7) v) + ) + ) +) + +(declare-datatypes (T) ( (List (Nil) (Cstr (head T) (tail List) ) ) ) ) +(declare-datatypes (T S) ( (Pair (Pair (first T) (second S)) ) ) ) + +(define-funs-rec + ( + (validList ((l (List (Pair Int Int)))) Bool) + ) + ( + (ite (= l (as Nil (List (Pair Int Int))) ) + true + (let ((hd (head l))) (and (>= (first hd) 0) + (validIdValue (first hd) (second hd)) + (validList (tail l)) + ) + ) + ) + ) +) + + +(declare-const myList (List (Pair Int Int))) +(assert (distinct myList (as Nil (List (Pair Int Int))))) +(assert (validList myList)) +(check-sat) diff --git a/test/regress/regress1/fmf/jasmin-cdt-crash.smt2 b/test/regress/regress1/fmf/jasmin-cdt-crash.smt2 new file mode 100644 index 000000000..7012838f9 --- /dev/null +++ b/test/regress/regress1/fmf/jasmin-cdt-crash.smt2 @@ -0,0 +1,100 @@ +; COMMAND-LINE: --finite-model-find --fmf-inst-engine --uf-ss-fair-monotone --lang=smt2.5 +; 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/regress1/fmf/ko-bound-set.cvc b/test/regress/regress1/fmf/ko-bound-set.cvc new file mode 100644 index 000000000..eebcbc2f8 --- /dev/null +++ b/test/regress/regress1/fmf/ko-bound-set.cvc @@ -0,0 +1,10 @@ +% EXPECT: invalid +OPTION "finite-model-find"; +OPTION "fmf-bound-int"; +OPTION "produce-models"; + +X, Y : SET OF INT; + +ASSERT FORALL(x : INT): x IS_IN X => x > 0; +QUERY ||X|| = 5 AND Y = X | {9} => ||Y|| <= 4; + diff --git a/test/regress/regress1/fmf/loopy_coda.smt2 b/test/regress/regress1/fmf/loopy_coda.smt2 new file mode 100644 index 000000000..519fb17fc --- /dev/null +++ b/test/regress/regress1/fmf/loopy_coda.smt2 @@ -0,0 +1,38 @@ +; COMMAND-LINE: --finite-model-find --fmf-inst-engine --uf-ss-fair-monotone --lang=smt2.5 +; 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) diff --git a/test/regress/regress1/fmf/lst-no-self-rev-exp.smt2 b/test/regress/regress1/fmf/lst-no-self-rev-exp.smt2 new file mode 100644 index 000000000..d55e15925 --- /dev/null +++ b/test/regress/regress1/fmf/lst-no-self-rev-exp.smt2 @@ -0,0 +1,35 @@ +; COMMAND-LINE: --finite-model-find --dt-rewrite-error-sel --lang=smt2.5 +; EXPECT: sat +(set-logic ALL_SUPPORTED) +(declare-datatypes () ((Nat (succ (pred Nat)) (zero)) (Lst (cons (hd Nat) (tl Lst)) (nil)))) + +(declare-fun app (Lst Lst) Lst) +(declare-fun rev (Lst) Lst) + +(declare-sort I_app 0) +(declare-sort I_rev 0) + +(declare-fun a () I_app) +(declare-fun b () I_app) +(assert (not (= a b))) + +(declare-fun app_0_3 (I_app) Lst) +(declare-fun app_1_4 (I_app) Lst) +(declare-fun rev_0_5 (I_rev) Lst) + +(declare-fun xs () Lst) + +(assert (and + +(forall ((?i I_app)) (= (app (app_0_3 ?i) (app_1_4 ?i)) (ite (is-cons (app_0_3 ?i)) (cons (hd (app_0_3 ?i)) (app (tl (app_0_3 ?i)) (app_1_4 ?i))) (app_1_4 ?i))) ) + +(forall ((?i I_rev)) (= (rev (rev_0_5 ?i)) (ite (is-cons (rev_0_5 ?i)) (app (rev (tl (rev_0_5 ?i))) (cons (hd (rev_0_5 ?i)) nil)) nil)) ) + +(forall ((?i I_rev)) (or (not (is-cons (rev_0_5 ?i))) (and (not (forall ((?z I_app)) (not (and (= (app_0_3 ?z) (rev (tl (rev_0_5 ?i)))) (= (app_1_4 ?z) (cons (hd (rev_0_5 ?i)) nil)))) )) (not (forall ((?z I_rev)) (not (= (rev_0_5 ?z) (tl (rev_0_5 ?i)) )) )))) ) + +(not (or (= xs (rev xs)) (forall ((?z I_rev)) (not (= (rev_0_5 ?z) xs)) ))) + +)) + +(check-sat) + diff --git a/test/regress/regress1/fmf/memory_model-R_cpp-dd.cvc b/test/regress/regress1/fmf/memory_model-R_cpp-dd.cvc new file mode 100644 index 000000000..5d1289997 --- /dev/null +++ b/test/regress/regress1/fmf/memory_model-R_cpp-dd.cvc @@ -0,0 +1,52 @@ +% EXPECT: sat +OPTION "produce-models"; +OPTION "fmf-bound"; + +DATATYPE MOPERATION = R | W | M END; +DATATYPE ORDER = I | SC | U END; +DATATYPE ATOM = AT | NA END; + +DATATYPE BINT = I0 | I1 | I2 | I3 END; + +DATATYPE TEAR_TYPE = TEAR_TRUE | TEAR_FALSE END; +SDBLOCK_TYPE: TYPE; +VALUE_TYPE: TYPE; +ADDRESS_TYPE: TYPE = SET OF BINT; + +MEM_OP_TYPE : TYPE = [# O:MOPERATION, T:TEAR_TYPE, R:ORDER, A:ATOM, B:SDBLOCK_TYPE, M:ADDRESS_TYPE, V:VALUE_TYPE #]; +EV_REL: TYPE = SET OF [MEM_OP_TYPE, MEM_OP_TYPE]; +THREAD_TYPE : TYPE = [# E:SET OF MEM_OP_TYPE, PO:EV_REL #]; + +m1 : SDBLOCK_TYPE; + +ow1 : MEM_OP_TYPE; +or2 : MEM_OP_TYPE; + +v1 : VALUE_TYPE; +v2 : VALUE_TYPE; + +ASSERT (ow1.O = W) AND + (ow1.T = TEAR_FALSE) AND + (ow1.R = U) AND + (ow1.A = NA) AND + (ow1.B = m1) AND + (ow1.M = {I0}) AND + (ow1.V = v1); + +ASSERT (or2.O = R) AND + (or2.T = TEAR_FALSE) AND + (or2.R = U) AND + (or2.A = NA) AND + (or2.B = m1) AND + (or2.M = {I0}) AND + (or2.V = v2); + +ev_set : SET OF MEM_OP_TYPE; + +ASSERT ev_set = {ow1, or2}; + +RF : EV_REL; + +ASSERT FORALL (r,w: MEM_OP_TYPE) : (((r IS_IN ev_set) AND (w IS_IN ev_set)) => (((r,w) IS_IN RF) <=> ((r.O = R) AND (w.O = W)))); + +CHECKSAT; diff --git a/test/regress/regress1/fmf/nun-0208-to.smt2 b/test/regress/regress1/fmf/nun-0208-to.smt2 new file mode 100644 index 000000000..e6b3c2021 --- /dev/null +++ b/test/regress/regress1/fmf/nun-0208-to.smt2 @@ -0,0 +1,180 @@ +; COMMAND-LINE: --finite-model-find --lang=smt2.5 +; EXPECT: sat + (set-logic ALL_SUPPORTED) + (declare-sort b__ 0) + (declare-fun __nun_card_witness_0_ () b__) + (declare-sort a__ 0) + (declare-fun __nun_card_witness_1_ () a__) + (declare-datatypes () + ((prod__ (Pair__ (_select_Pair___0 a__) (_select_Pair___1 b__))))) + (declare-datatypes () + ((list2__ + (Cons2__ (_select_Cons2___0 prod__) (_select_Cons2___1 list2__)) + (Nil2__ )))) + (declare-datatypes () + ((list__ (Cons__ (_select_Cons___0 a__) (_select_Cons___1 list__)) + (Nil__ )))) + (declare-datatypes () + ((list1__ (Cons1__ (_select_Cons1___0 b__) (_select_Cons1___1 list1__)) + (Nil1__ )))) + (declare-sort G_zip__ 0) + (declare-fun __nun_card_witness_2_ () G_zip__) + (declare-fun zip__ (list__ list1__) list2__) + (declare-fun proj_G_zip__0_ (G_zip__) list__) + (declare-fun proj_G_zip__1_ (G_zip__) list1__) + (assert + (forall ((a/166 G_zip__)) + (and + (= (zip__ (proj_G_zip__0_ a/166) (proj_G_zip__1_ a/166)) + (ite (is-Cons1__ (proj_G_zip__1_ a/166)) + (ite (is-Cons__ (proj_G_zip__0_ a/166)) + (Cons2__ + (Pair__ (_select_Cons___0 (proj_G_zip__0_ a/166)) + (_select_Cons1___0 (proj_G_zip__1_ a/166))) + (zip__ (_select_Cons___1 (proj_G_zip__0_ a/166)) + (_select_Cons1___1 (proj_G_zip__1_ a/166)))) + Nil2__) + Nil2__)) + (=> (is-Cons1__ (proj_G_zip__1_ a/166)) + (=> (is-Cons__ (proj_G_zip__0_ a/166)) + (exists ((a/168 G_zip__)) + (and + (= (_select_Cons1___1 (proj_G_zip__1_ a/166)) + (proj_G_zip__1_ a/168)) + (= (_select_Cons___1 (proj_G_zip__0_ a/166)) + (proj_G_zip__0_ a/168))))))))) + (declare-datatypes () ((nat__ (Suc__ (_select_Suc___0 nat__)) (zero__ )))) + (declare-sort G_replicate__ 0) + (declare-fun __nun_card_witness_3_ () G_replicate__) + (declare-fun replicate__ (nat__ a__) list__) + (declare-fun proj_G_replicate__0_ (G_replicate__) nat__) + (declare-fun proj_G_replicate__1_ (G_replicate__) a__) + (assert + (forall ((a/169 G_replicate__)) + (and + (= + (replicate__ (proj_G_replicate__0_ a/169) + (proj_G_replicate__1_ a/169)) + (ite (is-Suc__ (proj_G_replicate__0_ a/169)) + (Cons__ (proj_G_replicate__1_ a/169) + (replicate__ (_select_Suc___0 (proj_G_replicate__0_ a/169)) + (proj_G_replicate__1_ a/169))) + Nil__)) + (=> (is-Suc__ (proj_G_replicate__0_ a/169)) + (exists ((a/171 G_replicate__)) + (and + (= (proj_G_replicate__1_ a/169) (proj_G_replicate__1_ a/171)) + (= (_select_Suc___0 (proj_G_replicate__0_ a/169)) + (proj_G_replicate__0_ a/171)))))))) + (declare-fun j__ () nat__) + (declare-fun x__ () a__) + (declare-sort G_replicate1__ 0) + (declare-fun __nun_card_witness_4_ () G_replicate1__) + (declare-fun replicate1__ (nat__ b__) list1__) + (declare-fun proj_G_replicate1__0_ (G_replicate1__) nat__) + (declare-fun proj_G_replicate1__1_ (G_replicate1__) b__) + (assert + (forall ((a/172 G_replicate1__)) + (and + (= + (replicate1__ (proj_G_replicate1__0_ a/172) + (proj_G_replicate1__1_ a/172)) + (ite (is-Suc__ (proj_G_replicate1__0_ a/172)) + (Cons1__ (proj_G_replicate1__1_ a/172) + (replicate1__ (_select_Suc___0 (proj_G_replicate1__0_ a/172)) + (proj_G_replicate1__1_ a/172))) + Nil1__)) + (=> (is-Suc__ (proj_G_replicate1__0_ a/172)) + (exists ((a/174 G_replicate1__)) + (and + (= (proj_G_replicate1__1_ a/172) (proj_G_replicate1__1_ a/174)) + (= (_select_Suc___0 (proj_G_replicate1__0_ a/172)) + (proj_G_replicate1__0_ a/174)))))))) + (declare-fun y__ () b__) + (declare-sort G_replicate2__ 0) + (declare-fun __nun_card_witness_5_ () G_replicate2__) + (declare-fun replicate2__ (nat__ prod__) list2__) + (declare-fun proj_G_replicate2__0_ (G_replicate2__) nat__) + (declare-fun proj_G_replicate2__1_ (G_replicate2__) prod__) + (assert + (forall ((a/175 G_replicate2__)) + (and + (= + (replicate2__ (proj_G_replicate2__0_ a/175) + (proj_G_replicate2__1_ a/175)) + (ite (is-Suc__ (proj_G_replicate2__0_ a/175)) + (Cons2__ (proj_G_replicate2__1_ a/175) + (replicate2__ (_select_Suc___0 (proj_G_replicate2__0_ a/175)) + (proj_G_replicate2__1_ a/175))) + Nil2__)) + (=> (is-Suc__ (proj_G_replicate2__0_ a/175)) + (exists ((a/177 G_replicate2__)) + (and + (= (proj_G_replicate2__1_ a/175) (proj_G_replicate2__1_ a/177)) + (= (_select_Suc___0 (proj_G_replicate2__0_ a/175)) + (proj_G_replicate2__0_ a/177)))))))) + (declare-sort G_less__eq__ 0) + (declare-fun __nun_card_witness_6_ () G_less__eq__) + (declare-fun less__eq__ (nat__ nat__) Bool) + (declare-fun proj_G_less__eq__0_ (G_less__eq__) nat__) + (declare-fun proj_G_less__eq__1_ (G_less__eq__) nat__) + (assert + (forall ((a/178 G_less__eq__)) + (and + (= + (less__eq__ (proj_G_less__eq__0_ a/178) (proj_G_less__eq__1_ a/178)) + (=> (is-Suc__ (proj_G_less__eq__0_ a/178)) + (and (is-Suc__ (proj_G_less__eq__1_ a/178)) + (less__eq__ (_select_Suc___0 (proj_G_less__eq__0_ a/178)) + (_select_Suc___0 (proj_G_less__eq__1_ a/178)))))) + (exists ((a/182 G_less__eq__)) + (and + (= (_select_Suc___0 (proj_G_less__eq__1_ a/178)) + (proj_G_less__eq__1_ a/182)) + (= (_select_Suc___0 (proj_G_less__eq__0_ a/178)) + (proj_G_less__eq__0_ a/182))))))) + (declare-sort G_min__ 0) + (declare-fun __nun_card_witness_7_ () G_min__) + (declare-fun min__ (nat__ nat__) nat__) + (declare-fun proj_G_min__0_ (G_min__) nat__) + (declare-fun proj_G_min__1_ (G_min__) nat__) + (assert + (forall ((a/183 G_min__)) + (and + (= (min__ (proj_G_min__0_ a/183) (proj_G_min__1_ a/183)) + (ite (less__eq__ (proj_G_min__0_ a/183) (proj_G_min__1_ a/183)) + (proj_G_min__0_ a/183) (proj_G_min__1_ a/183))) + (exists ((a/184 G_less__eq__)) + (and (= (proj_G_min__1_ a/183) (proj_G_less__eq__1_ a/184)) + (= (proj_G_min__0_ a/183) (proj_G_less__eq__0_ a/184))))))) + (declare-fun i__ () nat__) + (assert + (not + (=> + (and + (exists ((a/212 G_min__)) + (and (= i__ (proj_G_min__1_ a/212)) (= i__ (proj_G_min__0_ a/212)))) + (exists ((a/208 G_replicate2__)) + (and (= (Pair__ x__ y__) (proj_G_replicate2__1_ a/208)) + (= (min__ i__ i__) (proj_G_replicate2__0_ a/208)) + (exists ((a/210 G_min__)) + (and (= i__ (proj_G_min__1_ a/210)) + (= i__ (proj_G_min__0_ a/210)))))) + (exists ((a/199 G_zip__)) + (and (= (replicate1__ j__ y__) (proj_G_zip__1_ a/199)) + (exists ((a/202 G_replicate1__)) + (and (= y__ (proj_G_replicate1__1_ a/202)) + (= j__ (proj_G_replicate1__0_ a/202)))) + (= (replicate__ j__ x__) (proj_G_zip__0_ a/199)) + (exists ((a/203 G_replicate__)) + (and (= x__ (proj_G_replicate__1_ a/203)) + (= j__ (proj_G_replicate__0_ a/203)))))) + (exists ((a/207 G_replicate1__)) + (and (= y__ (proj_G_replicate1__1_ a/207)) + (= j__ (proj_G_replicate1__0_ a/207)))) + (exists ((a/206 G_replicate__)) + (and (= x__ (proj_G_replicate__1_ a/206)) + (= j__ (proj_G_replicate__0_ a/206))))) + (= (replicate2__ (min__ i__ i__) (Pair__ x__ y__)) + (zip__ (replicate__ j__ x__) (replicate1__ j__ y__)))))) + (check-sat) diff --git a/test/regress/regress1/fmf/nunchaku2309663.nun.min.smt2 b/test/regress/regress1/fmf/nunchaku2309663.nun.min.smt2 deleted file mode 100644 index 9c8bc1d3e..000000000 --- a/test/regress/regress1/fmf/nunchaku2309663.nun.min.smt2 +++ /dev/null @@ -1,79 +0,0 @@ -; EXPECT: unsat -; COMMAND-LINE: --finite-model-find --lang=smt2.5 -(set-logic ALL_SUPPORTED) -(set-info :status unsat) -(declare-datatypes () ((nat__ (Suc__ (_select_Suc___0 nat__)) (zero__ )))) -(declare-sort a__ 0) -(declare-fun __nun_card_witness_0_ () a__) -(declare-datatypes () - ((tree__ - (MKT__ (_select_MKT___0 a__) (_select_MKT___1 tree__) - (_select_MKT___2 tree__) (_select_MKT___3 nat__)) - (ET__ )))) -(declare-sort G_plus__ 0) -(declare-fun __nun_card_witness_1_ () G_plus__) -(declare-fun plus__ (nat__ nat__) nat__) -(declare-fun proj_G_plus__0_ (G_plus__) nat__) -(declare-fun proj_G_plus__1_ (G_plus__) nat__) - -(declare-sort G_less__eq__ 0) -(declare-fun __nun_card_witness_2_ () G_less__eq__) -(declare-fun less__eq__ (nat__ nat__) Bool) -(declare-fun proj_G_less__eq__0_ (G_less__eq__) nat__) -(declare-fun proj_G_less__eq__1_ (G_less__eq__) nat__) - -(declare-sort G_max__ 0) -(declare-fun __nun_card_witness_3_ () G_max__) -(declare-fun max__ (nat__ nat__) nat__) -(declare-fun proj_G_max__0_ (G_max__) nat__) -(declare-fun proj_G_max__1_ (G_max__) nat__) - -(declare-sort G_one__ 0) -(declare-fun __nun_card_witness_4_ () G_one__) -(declare-fun one__ () nat__) -(assert (forall ((a/295 G_one__)) (= one__ (Suc__ zero__)))) -(declare-sort G_height__ 0) -(declare-fun __nun_card_witness_5_ () G_height__) -(declare-fun height__ (tree__) nat__) -(declare-fun proj_G_height__0_ (G_height__) tree__) - -(declare-sort G_avl__ 0) -(declare-fun __nun_card_witness_6_ () G_avl__) -(declare-fun avl__ (tree__) Bool) -(declare-fun proj_G_avl__0_ (G_avl__) tree__) - -(declare-fun l__ () tree__) -(declare-fun r__ () tree__) -(declare-sort G_minus__ 0) -(declare-fun __nun_card_witness_7_ () G_minus__) -(declare-fun minus__ (Bool Bool) Bool) -(declare-fun proj_G_minus__0_ (G_minus__) Bool) -(declare-fun proj_G_minus__1_ (G_minus__) Bool) - -(declare-sort G_ht__ 0) -(declare-fun __nun_card_witness_8_ () G_ht__) -(declare-fun ht__ (tree__) nat__) -(declare-fun proj_G_ht__0_ (G_ht__) tree__) - -(declare-sort G_mkt__ 0) -(declare-fun __nun_card_witness_9_ () G_mkt__) -(declare-fun mkt__ (a__ tree__ tree__) tree__) -(declare-fun proj_G_mkt__0_ (G_mkt__) a__) -(declare-fun proj_G_mkt__1_ (G_mkt__) tree__) -(declare-fun proj_G_mkt__2_ (G_mkt__) tree__) - -(declare-fun x__ () a__) - -(assert (and -(forall ((a/334 G_avl__)) (and (= (avl__ (proj_G_avl__0_ a/334)) (=> (is-MKT__ (proj_G_avl__0_ a/334)) (and (or (= (height__ (_select_MKT___1 (proj_G_avl__0_ a/334))) (height__ (_select_MKT___2 (proj_G_avl__0_ a/334)))) (= (height__ (_select_MKT___1 (proj_G_avl__0_ a/334))) (plus__ (height__ (_select_MKT___2 (proj_G_avl__0_ a/334))) one__)) (= (height__ (_select_MKT___2 (proj_G_avl__0_ a/334))) (plus__ (height__ (_select_MKT___1 (proj_G_avl__0_ a/334))) one__))) (= (_select_MKT___3 (proj_G_avl__0_ a/334)) (plus__ (max__ (height__ (_select_MKT___1 (proj_G_avl__0_ a/334))) (height__ (_select_MKT___2 (proj_G_avl__0_ a/334)))) one__)) (avl__ (_select_MKT___1 (proj_G_avl__0_ a/334))) (avl__ (_select_MKT___2 (proj_G_avl__0_ a/334)))))) (exists ((a/602 G_avl__)) (= (_select_MKT___2 (proj_G_avl__0_ a/334)) (proj_G_avl__0_ a/602)) ) (exists ((a/601 G_avl__)) (= (_select_MKT___1 (proj_G_avl__0_ a/334)) (proj_G_avl__0_ a/601)) ) (exists ((a/592 G_max__)) (and (= (height__ (_select_MKT___2 (proj_G_avl__0_ a/334))) (proj_G_max__1_ a/592)) (exists ((a/595 G_height__)) (= (_select_MKT___2 (proj_G_avl__0_ a/334)) (proj_G_height__0_ a/595)) ) (= (height__ (_select_MKT___1 (proj_G_avl__0_ a/334))) (proj_G_max__0_ a/592)) (exists ((a/596 G_height__)) (= (_select_MKT___1 (proj_G_avl__0_ a/334)) (proj_G_height__0_ a/596)) )) ) (exists ((a/600 G_height__)) (= (_select_MKT___2 (proj_G_avl__0_ a/334)) (proj_G_height__0_ a/600)) ) (exists ((a/599 G_height__)) (= (_select_MKT___1 (proj_G_avl__0_ a/334)) (proj_G_height__0_ a/599)) ) (exists ((a/564 G_plus__)) (and (= one__ (proj_G_plus__1_ a/564)) (= (max__ (height__ (_select_MKT___1 (proj_G_avl__0_ a/334))) (height__ (_select_MKT___2 (proj_G_avl__0_ a/334)))) (proj_G_plus__0_ a/564)) (exists ((a/581 G_height__)) (= (_select_MKT___1 (proj_G_avl__0_ a/334)) (proj_G_height__0_ a/581)) ) (exists ((a/582 G_height__)) (= (_select_MKT___2 (proj_G_avl__0_ a/334)) (proj_G_height__0_ a/582)) ) (exists ((a/574 G_max__)) (and (= (height__ (_select_MKT___2 (proj_G_avl__0_ a/334))) (proj_G_max__1_ a/574)) (exists ((a/577 G_height__)) (= (_select_MKT___2 (proj_G_avl__0_ a/334)) (proj_G_height__0_ a/577)) ) (= (height__ (_select_MKT___1 (proj_G_avl__0_ a/334))) (proj_G_max__0_ a/574)) (exists ((a/578 G_height__)) (= (_select_MKT___1 (proj_G_avl__0_ a/334)) (proj_G_height__0_ a/578)) )) )) ) (exists ((a/551 G_height__)) (= (_select_MKT___1 (proj_G_avl__0_ a/334)) (proj_G_height__0_ a/551)) ) (exists ((a/550 G_height__)) (= (_select_MKT___2 (proj_G_avl__0_ a/334)) (proj_G_height__0_ a/550)) ) (exists ((a/557 G_height__)) (= (_select_MKT___1 (proj_G_avl__0_ a/334)) (proj_G_height__0_ a/557)) ) (exists ((a/552 G_plus__)) (and (= one__ (proj_G_plus__1_ a/552)) (= (height__ (_select_MKT___2 (proj_G_avl__0_ a/334))) (proj_G_plus__0_ a/552)) (exists ((a/554 G_height__)) (= (_select_MKT___2 (proj_G_avl__0_ a/334)) (proj_G_height__0_ a/554)) )) ) (exists ((a/556 G_height__)) (= (_select_MKT___2 (proj_G_avl__0_ a/334)) (proj_G_height__0_ a/556)) ) (exists ((a/563 G_height__)) (= (_select_MKT___2 (proj_G_avl__0_ a/334)) (proj_G_height__0_ a/563)) ) (exists ((a/558 G_plus__)) (and (= one__ (proj_G_plus__1_ a/558)) (= (height__ (_select_MKT___1 (proj_G_avl__0_ a/334))) (proj_G_plus__0_ a/558)) (exists ((a/560 G_height__)) (= (_select_MKT___1 (proj_G_avl__0_ a/334)) (proj_G_height__0_ a/560)) )) ) (exists ((a/562 G_height__)) (= (_select_MKT___1 (proj_G_avl__0_ a/334)) (proj_G_height__0_ a/562)) )) ) -(forall ((a/603 G_minus__)) (= (minus__ (proj_G_minus__0_ a/603) (proj_G_minus__1_ a/603)) (ite (proj_G_minus__0_ a/603) (ite (proj_G_minus__1_ a/603) (and (proj_G_minus__0_ a/603) (not (proj_G_minus__1_ a/603))) (and (proj_G_minus__0_ a/603) (not (proj_G_minus__1_ a/603)))) (ite (proj_G_minus__1_ a/603) (and (proj_G_minus__0_ a/603) (not (proj_G_minus__1_ a/603))) (and (proj_G_minus__0_ a/603) (not (proj_G_minus__1_ a/603)))))) ) -(forall ((a/296 G_height__)) (and (= (height__ (proj_G_height__0_ a/296)) (ite (is-MKT__ (proj_G_height__0_ a/296)) (plus__ (max__ (height__ (_select_MKT___1 (proj_G_height__0_ a/296))) (height__ (_select_MKT___2 (proj_G_height__0_ a/296)))) one__) zero__)) (=> (is-MKT__ (proj_G_height__0_ a/296)) (and (exists ((a/297 G_plus__)) (and (= one__ (proj_G_plus__1_ a/297)) (= (max__ (height__ (_select_MKT___1 (proj_G_height__0_ a/296))) (height__ (_select_MKT___2 (proj_G_height__0_ a/296)))) (proj_G_plus__0_ a/297)) (exists ((a/314 G_height__)) (= (_select_MKT___1 (proj_G_height__0_ a/296)) (proj_G_height__0_ a/314)) ) (exists ((a/315 G_height__)) (= (_select_MKT___2 (proj_G_height__0_ a/296)) (proj_G_height__0_ a/315)) ) (exists ((a/307 G_max__)) (and (= (height__ (_select_MKT___2 (proj_G_height__0_ a/296))) (proj_G_max__1_ a/307)) (exists ((a/310 G_height__)) (= (_select_MKT___2 (proj_G_height__0_ a/296)) (proj_G_height__0_ a/310)) ) (= (height__ (_select_MKT___1 (proj_G_height__0_ a/296))) (proj_G_max__0_ a/307)) (exists ((a/311 G_height__)) (= (_select_MKT___1 (proj_G_height__0_ a/296)) (proj_G_height__0_ a/311)) )) )) ) (exists ((a/332 G_height__)) (= (_select_MKT___1 (proj_G_height__0_ a/296)) (proj_G_height__0_ a/332)) ) (exists ((a/333 G_height__)) (= (_select_MKT___2 (proj_G_height__0_ a/296)) (proj_G_height__0_ a/333)) ) (exists ((a/325 G_max__)) (and (= (height__ (_select_MKT___2 (proj_G_height__0_ a/296))) (proj_G_max__1_ a/325)) (exists ((a/328 G_height__)) (= (_select_MKT___2 (proj_G_height__0_ a/296)) (proj_G_height__0_ a/328)) ) (= (height__ (_select_MKT___1 (proj_G_height__0_ a/296))) (proj_G_max__0_ a/325)) (exists ((a/329 G_height__)) (= (_select_MKT___1 (proj_G_height__0_ a/296)) (proj_G_height__0_ a/329)) )) )))) ) -(forall ((a/604 G_ht__)) (= (ht__ (proj_G_ht__0_ a/604)) (ite (is-MKT__ (proj_G_ht__0_ a/604)) (_select_MKT___3 (proj_G_ht__0_ a/604)) zero__)) ) - -(not (=> (and (avl__ l__) (exists ((a/1961 G_avl__)) (= l__ (proj_G_avl__0_ a/1961)) )) (=> (and (avl__ r__) (exists ((a/2175 G_avl__)) (= r__ (proj_G_avl__0_ a/2175)) )) (=> (or (and (= (height__ l__) (height__ r__)) (exists ((a/2334 G_height__)) (= l__ (proj_G_height__0_ a/2334)) ) (exists ((a/2333 G_height__)) (= r__ (proj_G_height__0_ a/2333)) )) (and (minus__ (= (height__ l__) (plus__ (height__ r__) one__)) (= (height__ r__) (plus__ (height__ l__) one__))) (exists ((a/2382 G_height__)) (= l__ (proj_G_height__0_ a/2382)) ) (exists ((a/2378 G_plus__)) (and (= one__ (proj_G_plus__1_ a/2378)) (= (height__ l__) (proj_G_plus__0_ a/2378)) (exists ((a/2380 G_height__)) (= l__ (proj_G_height__0_ a/2380)) )) ) (exists ((a/2383 G_height__)) (= r__ (proj_G_height__0_ a/2383)) ) (exists ((a/2376 G_height__)) (= r__ (proj_G_height__0_ a/2376)) ) (exists ((a/2372 G_plus__)) (and (= one__ (proj_G_plus__1_ a/2372)) (= (height__ r__) (proj_G_plus__0_ a/2372)) (exists ((a/2374 G_height__)) (= r__ (proj_G_height__0_ a/2374)) )) ) (exists ((a/2377 G_height__)) (= l__ (proj_G_height__0_ a/2377)) ) (exists ((a/2335 G_minus__)) (and (= (= (height__ r__) (plus__ (height__ l__) one__)) (proj_G_minus__1_ a/2335)) (exists ((a/2352 G_height__)) (= l__ (proj_G_height__0_ a/2352)) ) (exists ((a/2348 G_plus__)) (and (= one__ (proj_G_plus__1_ a/2348)) (= (height__ l__) (proj_G_plus__0_ a/2348)) (exists ((a/2350 G_height__)) (= l__ (proj_G_height__0_ a/2350)) )) ) (exists ((a/2353 G_height__)) (= r__ (proj_G_height__0_ a/2353)) ) (= (= (height__ l__) (plus__ (height__ r__) one__)) (proj_G_minus__0_ a/2335)) (exists ((a/2358 G_height__)) (= r__ (proj_G_height__0_ a/2358)) ) (exists ((a/2354 G_plus__)) (and (= one__ (proj_G_plus__1_ a/2354)) (= (height__ r__) (proj_G_plus__0_ a/2354)) (exists ((a/2356 G_height__)) (= r__ (proj_G_height__0_ a/2356)) )) ) (exists ((a/2359 G_height__)) (= l__ (proj_G_height__0_ a/2359)) )) ))) (=> (exists ((a/2384 G_avl__)) (and (= (mkt__ x__ l__ r__) (proj_G_avl__0_ a/2384)) (exists ((a/2385 G_mkt__)) (and (= r__ (proj_G_mkt__2_ a/2385)) (= l__ (proj_G_mkt__1_ a/2385)) (= x__ (proj_G_mkt__0_ a/2385))) )) ) (=> (exists ((a/2387 G_mkt__)) (and (= r__ (proj_G_mkt__2_ a/2387)) (= l__ (proj_G_mkt__1_ a/2387)) (= x__ (proj_G_mkt__0_ a/2387))) ) (avl__ (mkt__ x__ l__ r__)))))))) -(forall ((a/605 G_mkt__)) (and (= (mkt__ (proj_G_mkt__0_ a/605) (proj_G_mkt__1_ a/605) (proj_G_mkt__2_ a/605)) (MKT__ (proj_G_mkt__0_ a/605) (proj_G_mkt__1_ a/605) (proj_G_mkt__2_ a/605) (plus__ (max__ (ht__ (proj_G_mkt__1_ a/605)) (ht__ (proj_G_mkt__2_ a/605))) one__))) (exists ((a/671 G_max__)) (and (= (ht__ (proj_G_mkt__2_ a/605)) (proj_G_max__1_ a/671)) (exists ((a/674 G_ht__)) (= (proj_G_mkt__2_ a/605) (proj_G_ht__0_ a/674)) ) (= (ht__ (proj_G_mkt__1_ a/605)) (proj_G_max__0_ a/671)) (exists ((a/675 G_ht__)) (= (proj_G_mkt__1_ a/605) (proj_G_ht__0_ a/675)) )) ) (exists ((a/679 G_ht__)) (= (proj_G_mkt__2_ a/605) (proj_G_ht__0_ a/679)) ) (exists ((a/678 G_ht__)) (= (proj_G_mkt__1_ a/605) (proj_G_ht__0_ a/678)) ) (exists ((a/643 G_plus__)) (and (= one__ (proj_G_plus__1_ a/643)) (= (max__ (ht__ (proj_G_mkt__1_ a/605)) (ht__ (proj_G_mkt__2_ a/605))) (proj_G_plus__0_ a/643)) (exists ((a/660 G_ht__)) (= (proj_G_mkt__1_ a/605) (proj_G_ht__0_ a/660)) ) (exists ((a/661 G_ht__)) (= (proj_G_mkt__2_ a/605) (proj_G_ht__0_ a/661)) ) (exists ((a/653 G_max__)) (and (= (ht__ (proj_G_mkt__2_ a/605)) (proj_G_max__1_ a/653)) (exists ((a/656 G_ht__)) (= (proj_G_mkt__2_ a/605) (proj_G_ht__0_ a/656)) ) (= (ht__ (proj_G_mkt__1_ a/605)) (proj_G_max__0_ a/653)) (exists ((a/657 G_ht__)) (= (proj_G_mkt__1_ a/605) (proj_G_ht__0_ a/657)) )) )) )) ) -(forall ((a/295 G_one__)) (= one__ (Suc__ zero__)) ) - -)) - -(check-sat) diff --git a/test/regress/regress1/fmf/pow2-bool.smt2 b/test/regress/regress1/fmf/pow2-bool.smt2 new file mode 100644 index 000000000..4943c646c --- /dev/null +++ b/test/regress/regress1/fmf/pow2-bool.smt2 @@ -0,0 +1,17 @@ +; COMMAND-LINE: --fmf-fun --no-check-models +; EXPECT: sat +(set-logic ALL) + +(define-fun-rec pow2 ((n Int) (p Int)) Bool ( + or + (and (= n 0) (= p 1)) + (and (> n 0) (> p 1) (= 0 (mod p 2)) (pow2 (- n 1) (div p 2))) +)) + +(declare-const n Int) +(declare-const p Int) + +(assert (= n 10)) +(assert (pow2 n p)) + +(check-sat) diff --git a/test/regress/regress1/fmf/refcount24.cvc.smt2 b/test/regress/regress1/fmf/refcount24.cvc.smt2 new file mode 100644 index 000000000..e3b6957d0 --- /dev/null +++ b/test/regress/regress1/fmf/refcount24.cvc.smt2 @@ -0,0 +1,37 @@ +; COMMAND-LINE: --finite-model-find +; EXPECT: sat +(set-logic ALL_SUPPORTED) +(set-info :smt-lib-version 2.0) +(set-info :category "unknown") +(set-info :status sat) +(declare-datatypes () +((UNIT (Unit)) +)) +(declare-datatypes () +((BOOL (Truth) (Falsity)) +)) +(declare-sort resource$type 0) +(declare-sort process$type 0) +(declare-fun null () resource$type) +(declare-sort S$t$type 0) +(declare-fun S$empty () S$t$type) +(declare-fun S$mem (process$type S$t$type) BOOL) +(declare-fun S$add (process$type S$t$type) S$t$type) +(declare-fun S$remove (process$type S$t$type) S$t$type) +(declare-fun S$cardinality (S$t$type) Int) +(assert (forall ((e process$type)) (not (= (S$mem e S$empty) Truth)))) +(assert (forall ((x process$type) (y process$type) (s S$t$type)) (= (S$mem x (S$add y s)) (ite (or (= x y) (= (S$mem x s) Truth)) Truth Falsity)))) +(assert (forall ((x process$type) (y process$type) (s S$t$type)) (= (S$mem x (S$remove y s)) (ite (and (not (= x y)) (= (S$mem x s) Truth)) Truth Falsity)))) +(assert (= (S$cardinality S$empty) 0)) +(assert (forall ((s S$t$type)) (=> (= (S$cardinality s) 0) (= s S$empty)))) +(assert (forall ((s S$t$type)) (>= (S$cardinality s) 0))) +(assert (forall ((x process$type) (s S$t$type)) (let ((?v_0 (S$cardinality s))) (= (S$cardinality (S$add x s)) (ite (= (S$mem x s) Truth) ?v_0 (+ ?v_0 1)))))) +(assert (forall ((x process$type) (s S$t$type)) (let ((?v_0 (S$cardinality s))) (= (S$cardinality (S$remove x s)) (ite (= (S$mem x s) Truth) (- ?v_0 1) ?v_0))))) +(declare-fun count () (Array resource$type Int)) +(declare-fun ref () (Array process$type resource$type)) +(declare-fun valid () (Array resource$type BOOL)) +(declare-fun destroy$r () resource$type) +(declare-fun valid$1 () (Array resource$type BOOL)) +(assert (not (=> (forall ((p process$type)) (let ((?v_0 (select ref p))) (=> (not (= ?v_0 null)) (= (select valid ?v_0) Truth)))) (=> (not (= destroy$r null)) (=> (= (select valid destroy$r) Truth) (=> (= (select count destroy$r) 0) (=> (= valid$1 (store valid destroy$r Falsity)) (forall ((p process$type)) (let ((?v_1 (select ref p))) (=> (not (= ?v_1 null)) (= (select valid$1 ?v_1) Truth))))))))))) +(check-sat) +(exit) diff --git a/test/regress/regress1/fmf/sc-crash-052316.smt2 b/test/regress/regress1/fmf/sc-crash-052316.smt2 new file mode 100644 index 000000000..345d8220e --- /dev/null +++ b/test/regress/regress1/fmf/sc-crash-052316.smt2 @@ -0,0 +1,35 @@ +; COMMAND-LINE: --finite-model-find --lang=smt2.5 +; EXPECT: unsat + (set-logic ALL_SUPPORTED) + (set-info :status unsat) + (declare-sort g_ 0) + (declare-fun __nun_card_witness_0_ () g_) + (declare-sort f_ 0) + (declare-fun __nun_card_witness_1_ () f_) + (declare-sort e_ 0) + (declare-fun __nun_card_witness_2_ () e_) +(declare-datatypes () + ((prod1_ (Pair1_ (_select_Pair1__0 e_) (_select_Pair1__1 f_))))) + (declare-sort d_ 0) + (declare-fun __nun_card_witness_3_ () d_) + (declare-sort c_ 0) + (declare-fun __nun_card_witness_4_ () c_) + (declare-sort b_ 0) + (declare-fun __nun_card_witness_5_ () b_) + (declare-sort a_ 0) + (declare-fun __nun_card_witness_6_ () a_) +(declare-datatypes () + ((prod_ (Pair_ (_select_Pair__0 a_) (_select_Pair__1 b_))))) + (declare-fun f1_ (prod_ c_ d_ prod1_) g_) + (declare-fun g1_ (prod_) c_) + (declare-fun h_ (prod_ d_) prod1_) + (declare-fun nun_sk_0_ () prod_) +(declare-fun nun_sk_1_ (c_) d_) + (assert + (not + (exists ((v/72 c_)) + (exists ((x/73 prod1_)) + (= (f1_ nun_sk_0_ v/72 (nun_sk_1_ v/72) x/73) + (f1_ nun_sk_0_ (g1_ nun_sk_0_) (nun_sk_1_ v/72) + (h_ nun_sk_0_ (nun_sk_1_ v/72)))))))) +(check-sat) diff --git a/test/regress/regress1/fmf/with-ind-104-core.smt2 b/test/regress/regress1/fmf/with-ind-104-core.smt2 new file mode 100644 index 000000000..c1d718403 --- /dev/null +++ b/test/regress/regress1/fmf/with-ind-104-core.smt2 @@ -0,0 +1,35 @@ +; COMMAND-LINE: --lang=smt2.5 +; EXPECT: unsat +(set-logic ALL_SUPPORTED) +(set-info :status unsat) +(declare-datatypes () ((Nat!2409 (succ!2410 (pred!2411 Nat!2409)) (zero!2412)) +)) +(declare-datatypes () ((Lst!2413 (cons!2414 (head!2415 Nat!2409) (tail!2416 Lst!2413)) (nil!2417)) +)) +(declare-fun error_value!2418 () Nat!2409) +(declare-fun plus!237 (Nat!2409 Nat!2409) Nat!2409) +(declare-fun error_value!2419 () Nat!2409) +(declare-fun count!263 (Nat!2409 Lst!2413) Nat!2409) +(declare-fun pred!2411_uf_1 (Nat!2409) Nat!2409) +(declare-fun tail!2416_uf_2 (Lst!2413) Lst!2413) +(declare-fun head!2415_uf_3 (Lst!2413) Nat!2409) +(declare-sort I_plus!237 0) +(set-info :notes "plus!237_arg_0_4 is op created during fun def fmf") +(declare-fun plus!237_arg_0_4 (I_plus!237) Nat!2409) +(set-info :notes "plus!237_arg_1_5 is op created during fun def fmf") +(declare-fun plus!237_arg_1_5 (I_plus!237) Nat!2409) +(declare-sort I_count!263 0) +(set-info :notes "count!263_arg_0_6 is op created during fun def fmf") +(declare-fun count!263_arg_0_6 (I_count!263) Nat!2409) +(set-info :notes "count!263_arg_1_7 is op created during fun def fmf") +(declare-fun count!263_arg_1_7 (I_count!263) Lst!2413) +(assert +(and +(not (forall ((h!413 Nat!2409) (BOUND_VARIABLE_663 I_plus!237) (BOUND_VARIABLE_671 I_count!263) (BOUND_VARIABLE_679 I_count!263) (BOUND_VARIABLE_687 I_count!263) (BOUND_VARIABLE_695 I_plus!237) (BOUND_VARIABLE_703 I_count!263) (BOUND_VARIABLE_711 I_count!263) (BOUND_VARIABLE_719 I_count!263)) (or (not (= (plus!237 (count!263 (count!263_arg_0_6 BOUND_VARIABLE_671) (cons!2414 h!413 nil!2417)) (count!263 (count!263_arg_0_6 BOUND_VARIABLE_671) (count!263_arg_1_7 BOUND_VARIABLE_679))) (count!263 (count!263_arg_0_6 BOUND_VARIABLE_671) (cons!2414 h!413 (count!263_arg_1_7 BOUND_VARIABLE_679))))) (= (plus!237 (count!263 (succ!2410 (count!263_arg_0_6 BOUND_VARIABLE_671)) (cons!2414 h!413 nil!2417)) (count!263 (succ!2410 (count!263_arg_0_6 BOUND_VARIABLE_671)) (count!263_arg_1_7 BOUND_VARIABLE_679))) (count!263 (succ!2410 (count!263_arg_0_6 BOUND_VARIABLE_671)) (cons!2414 h!413 (count!263_arg_1_7 BOUND_VARIABLE_679)))) (not (= (plus!237_arg_0_4 BOUND_VARIABLE_663) (count!263 (count!263_arg_0_6 BOUND_VARIABLE_671) (cons!2414 h!413 nil!2417)))) (not (= (plus!237_arg_1_5 BOUND_VARIABLE_663) (count!263 (count!263_arg_0_6 BOUND_VARIABLE_671) (count!263_arg_1_7 BOUND_VARIABLE_679)))) (not (= (count!263_arg_1_7 BOUND_VARIABLE_671) (cons!2414 h!413 nil!2417))) (not (= (count!263_arg_0_6 BOUND_VARIABLE_679) (count!263_arg_0_6 BOUND_VARIABLE_671))) (not (= (count!263_arg_0_6 BOUND_VARIABLE_687) (count!263_arg_0_6 BOUND_VARIABLE_671))) (not (= (count!263_arg_1_7 BOUND_VARIABLE_687) (cons!2414 h!413 (count!263_arg_1_7 BOUND_VARIABLE_679)))) (not (= (plus!237_arg_0_4 BOUND_VARIABLE_695) (count!263 (succ!2410 (count!263_arg_0_6 BOUND_VARIABLE_671)) (cons!2414 h!413 nil!2417)))) (not (= (plus!237_arg_1_5 BOUND_VARIABLE_695) (count!263 (succ!2410 (count!263_arg_0_6 BOUND_VARIABLE_671)) (count!263_arg_1_7 BOUND_VARIABLE_679)))) (not (= (count!263_arg_0_6 BOUND_VARIABLE_703) (succ!2410 (count!263_arg_0_6 BOUND_VARIABLE_671)))) (not (= (count!263_arg_1_7 BOUND_VARIABLE_703) (cons!2414 h!413 nil!2417))) (not (= (count!263_arg_0_6 BOUND_VARIABLE_711) (succ!2410 (count!263_arg_0_6 BOUND_VARIABLE_671)))) (not (= (count!263_arg_1_7 BOUND_VARIABLE_711) (count!263_arg_1_7 BOUND_VARIABLE_679))) (not (= (count!263_arg_0_6 BOUND_VARIABLE_719) (succ!2410 (count!263_arg_0_6 BOUND_VARIABLE_671)))) (not (= (count!263_arg_1_7 BOUND_VARIABLE_719) (cons!2414 h!413 (count!263_arg_1_7 BOUND_VARIABLE_679))))) )) +(forall ((?j I_plus!237)) (= (plus!237 (plus!237_arg_0_4 ?j) (plus!237_arg_1_5 ?j)) (ite (is-zero!2412 (plus!237_arg_0_4 ?j)) (plus!237_arg_1_5 ?j) (ite (is-succ!2410 (plus!237_arg_0_4 ?j)) (succ!2410 (plus!237 (ite (is-succ!2410 (plus!237_arg_0_4 ?j)) (pred!2411 (plus!237_arg_0_4 ?j)) (pred!2411_uf_1 (plus!237_arg_0_4 ?j))) (plus!237_arg_1_5 ?j))) error_value!2418))) ) +(forall ((?i I_plus!237)) (ite (is-zero!2412 (plus!237_arg_0_4 ?i)) true (ite (is-succ!2410 (plus!237_arg_0_4 ?i)) (not (forall ((?z I_plus!237)) (or (not (= (plus!237_arg_0_4 ?z) (ite (is-succ!2410 (plus!237_arg_0_4 ?i)) (pred!2411 (plus!237_arg_0_4 ?i)) (pred!2411_uf_1 (plus!237_arg_0_4 ?i))))) (not (= (plus!237_arg_1_5 ?z) (plus!237_arg_1_5 ?i)))) )) true)) ) +(forall ((?i I_count!263)) (= (count!263 (count!263_arg_0_6 ?i) (count!263_arg_1_7 ?i)) (ite (is-nil!2417 (count!263_arg_1_7 ?i)) zero!2412 (ite (is-cons!2414 (count!263_arg_1_7 ?i)) (ite (= (count!263_arg_0_6 ?i) (ite (is-cons!2414 (count!263_arg_1_7 ?i)) (head!2415 (count!263_arg_1_7 ?i)) (head!2415_uf_3 (count!263_arg_1_7 ?i)))) (succ!2410 (count!263 (count!263_arg_0_6 ?i) (ite (is-cons!2414 (count!263_arg_1_7 ?i)) (tail!2416 (count!263_arg_1_7 ?i)) (tail!2416_uf_2 (count!263_arg_1_7 ?i))))) (count!263 (count!263_arg_0_6 ?i) (ite (is-cons!2414 (count!263_arg_1_7 ?i)) (tail!2416 (count!263_arg_1_7 ?i)) (tail!2416_uf_2 (count!263_arg_1_7 ?i))))) error_value!2419))) ) +(forall ((?j I_count!263)) (ite (is-nil!2417 (count!263_arg_1_7 ?j)) true (ite (is-cons!2414 (count!263_arg_1_7 ?j)) (ite (= (count!263_arg_0_6 ?j) (ite (is-cons!2414 (count!263_arg_1_7 ?j)) (head!2415 (count!263_arg_1_7 ?j)) (head!2415_uf_3 (count!263_arg_1_7 ?j)))) (not (forall ((?z I_count!263)) (or (not (= (count!263_arg_0_6 ?z) (count!263_arg_0_6 ?j))) (not (= (count!263_arg_1_7 ?z) (ite (is-cons!2414 (count!263_arg_1_7 ?j)) (tail!2416 (count!263_arg_1_7 ?j)) (tail!2416_uf_2 (count!263_arg_1_7 ?j)))))) )) (not (forall ((?z I_count!263)) (or (not (= (count!263_arg_0_6 ?z) (count!263_arg_0_6 ?j))) (not (= (count!263_arg_1_7 ?z) (ite (is-cons!2414 (count!263_arg_1_7 ?j)) (tail!2416 (count!263_arg_1_7 ?j)) (tail!2416_uf_2 (count!263_arg_1_7 ?j)))))) ))) true)) ) +) +) +(check-sat) |