diff options
| author | PaulMeng <baolmeng@gmail.com> | 2016-04-20 14:43:18 -0500 |
|---|---|---|
| committer | PaulMeng <baolmeng@gmail.com> | 2016-04-20 14:43:18 -0500 |
| commit | 904ffb6e73402bae537aa89e7fd8f0ab2e9d60e2 (patch) | |
| tree | d96bb0c974bdea6170957d3e39d47a98f5c85ca0 /test | |
| parent | a0054e9cc78822416d745e955c30f69cbb2a3aa7 (diff) | |
update from the master
Diffstat (limited to 'test')
93 files changed, 1043 insertions, 396 deletions
diff --git a/test/regress/regress0/fmf/ForElimination-scala-9.smt2 b/test/regress/regress0/fmf/ForElimination-scala-9.smt2 new file mode 100644 index 000000000..36bb915f4 --- /dev/null +++ b/test/regress/regress0/fmf/ForElimination-scala-9.smt2 @@ -0,0 +1,31 @@ +; COMMAND-LINE: --finite-model-find --uf-ss=no-minimal +; EXPECT: unsat +(set-logic ALL_SUPPORTED) +(declare-datatypes () ((Statement!1556 (Assign!1557 (varID!1558 (_ BitVec 32)) (expr!1559 Expression!1578)) (Block!1560 (body!1561 List!1617)) (For!1562 (init!1563 Statement!1556) (expr!1564 Expression!1578) (step!1565 Statement!1556) (body!1566 Statement!1556)) (IfThenElse!1567 (expr!1568 Expression!1578) (then!1569 Statement!1556) (elze!1570 Statement!1556)) (Print!1571 (msg!1572 (_ BitVec 32)) (varID!1573 (_ BitVec 32))) (Skip!1574) (While!1575 (expr!1576 Expression!1578) (body!1577 Statement!1556))) +(Expression!1578 (And!1579 (lhs!1580 Expression!1578) (rhs!1581 Expression!1578)) (Division!1582 (lhs!1583 Expression!1578) (rhs!1584 Expression!1578)) (Equals!1585 (lhs!1586 Expression!1578) (rhs!1587 Expression!1578)) (GreaterThan!1588 (lhs!1589 Expression!1578) (rhs!1590 Expression!1578)) (IntLiteral!1591 (value!1592 (_ BitVec 32))) (LessThan!1593 (lhs!1594 Expression!1578) (rhs!1595 Expression!1578)) (Minus!1596 (lhs!1597 Expression!1578) (rhs!1598 Expression!1578)) (Modulo!1599 (lhs!1600 Expression!1578) (rhs!1601 Expression!1578)) (Neg!1602 (expr!1603 Expression!1578)) (Not!1604 (expr!1605 Expression!1578)) (Or!1606 (lhs!1607 Expression!1578) (rhs!1608 Expression!1578)) (Plus!1609 (lhs!1610 Expression!1578) (rhs!1611 Expression!1578)) (Times!1612 (lhs!1613 Expression!1578) (rhs!1614 Expression!1578)) (Var!1615 (varID!1616 (_ BitVec 32)))) +(List!1617 (Cons!1618 (head!1619 Statement!1556) (tail!1620 List!1617)) (Nil!1621)) +)) +(declare-fun error_value!1622 () Bool) +(declare-fun ifree (Statement!1556) Bool) +(declare-fun isForFreeList!223 (List!1617) Bool) +(declare-fun error_value!1623 () List!1617) +(declare-fun efll (List!1617) List!1617) +(declare-fun efl (Statement!1556) Statement!1556) +(declare-sort I_ifree 0) +(set-info :notes "ifree_arg_0_1 is op created during fun def fmf") +(declare-fun ifree_arg_0_1 (I_ifree) Statement!1556) +(declare-sort I_isForFreeList!223 0) +(set-info :notes "isForFreeList!223_arg_0_2 is op created during fun def fmf") +(declare-fun isForFreeList!223_arg_0_2 (I_isForFreeList!223) List!1617) +(declare-sort I_efll 0) +(set-info :notes "efll_arg_0_3 is op created during fun def fmf") +(declare-fun efll_arg_0_3 (I_efll) List!1617) +(declare-sort I_efl 0) +(set-info :notes "efl_arg_0_4 is op created during fun def fmf") +(declare-fun efl_arg_0_4 (I_efl) Statement!1556) +(assert (forall ((?i I_ifree)) (and (= (ifree (ifree_arg_0_1 ?i)) (ite (is-Block!1560 (ifree_arg_0_1 ?i)) (isForFreeList!223 (body!1561 (ifree_arg_0_1 ?i))) (ite (is-IfThenElse!1567 (ifree_arg_0_1 ?i)) (and (ifree (elze!1570 (ifree_arg_0_1 ?i))) (ifree (then!1569 (ifree_arg_0_1 ?i)))) (ite (is-While!1575 (ifree_arg_0_1 ?i)) (ifree (body!1577 (ifree_arg_0_1 ?i))) (not (is-For!1562 (ifree_arg_0_1 ?i))))))) (ite (is-Block!1560 (ifree_arg_0_1 ?i)) (not (forall ((?z I_isForFreeList!223)) (not (= (isForFreeList!223_arg_0_2 ?z) (body!1561 (ifree_arg_0_1 ?i)))) )) (ite (is-IfThenElse!1567 (ifree_arg_0_1 ?i)) (and (not (forall ((?z I_ifree)) (not (= (ifree_arg_0_1 ?z) (elze!1570 (ifree_arg_0_1 ?i)))) )) (not (forall ((?z I_ifree)) (not (= (ifree_arg_0_1 ?z) (then!1569 (ifree_arg_0_1 ?i)))) ))) (ite (is-While!1575 (ifree_arg_0_1 ?i)) (not (forall ((?z I_ifree)) (not (= (ifree_arg_0_1 ?z) (body!1577 (ifree_arg_0_1 ?i)))) )) true)))) )) +(assert (forall ((?i I_isForFreeList!223)) (and (= (isForFreeList!223 (isForFreeList!223_arg_0_2 ?i)) (ite (is-Nil!1621 (isForFreeList!223_arg_0_2 ?i)) true (ite (is-Cons!1618 (isForFreeList!223_arg_0_2 ?i)) (and (isForFreeList!223 (tail!1620 (isForFreeList!223_arg_0_2 ?i))) (ifree (head!1619 (isForFreeList!223_arg_0_2 ?i)))) error_value!1622))) (ite (is-Nil!1621 (isForFreeList!223_arg_0_2 ?i)) true (ite (is-Cons!1618 (isForFreeList!223_arg_0_2 ?i)) (and (not (forall ((?z I_isForFreeList!223)) (not (= (isForFreeList!223_arg_0_2 ?z) (tail!1620 (isForFreeList!223_arg_0_2 ?i)))) )) (not (forall ((?z I_ifree)) (not (= (ifree_arg_0_1 ?z) (head!1619 (isForFreeList!223_arg_0_2 ?i)))) ))) true))) )) +(assert (forall ((?i I_efll)) (and (= (efll (efll_arg_0_3 ?i)) (ite (is-Nil!1621 (efll_arg_0_3 ?i)) Nil!1621 (ite (is-Cons!1618 (efll_arg_0_3 ?i)) (Cons!1618 (efl (head!1619 (efll_arg_0_3 ?i))) (efll (tail!1620 (efll_arg_0_3 ?i)))) error_value!1623))) (ite (is-Nil!1621 (efll_arg_0_3 ?i)) true (ite (is-Cons!1618 (efll_arg_0_3 ?i)) (and (not (forall ((?z I_efl)) (not (= (efl_arg_0_4 ?z) (head!1619 (efll_arg_0_3 ?i)))) )) (not (forall ((?z I_efll)) (not (= (efll_arg_0_3 ?z) (tail!1620 (efll_arg_0_3 ?i)))) ))) true))) )) +(assert (forall ((?i I_efl)) (and (= (efl (efl_arg_0_4 ?i)) (ite (is-Block!1560 (efl_arg_0_4 ?i)) (Block!1560 (efll (body!1561 (efl_arg_0_4 ?i)))) (ite (is-IfThenElse!1567 (efl_arg_0_4 ?i)) (IfThenElse!1567 (expr!1568 (efl_arg_0_4 ?i)) (efl (then!1569 (efl_arg_0_4 ?i))) (efl (elze!1570 (efl_arg_0_4 ?i)))) (ite (is-While!1575 (efl_arg_0_4 ?i)) (While!1575 (expr!1576 (efl_arg_0_4 ?i)) (efl (body!1577 (efl_arg_0_4 ?i)))) (ite (is-For!1562 (efl_arg_0_4 ?i)) (Block!1560 (Cons!1618 (efl (init!1563 (efl_arg_0_4 ?i))) (Cons!1618 (While!1575 (expr!1564 (efl_arg_0_4 ?i)) (Block!1560 (Cons!1618 (efl (body!1566 (efl_arg_0_4 ?i))) (Cons!1618 (efl (step!1565 (efl_arg_0_4 ?i))) Nil!1621)))) Nil!1621))) (efl_arg_0_4 ?i)))))) (ite (is-Block!1560 (efl_arg_0_4 ?i)) (not (forall ((?z I_efll)) (not (= (efll_arg_0_3 ?z) (body!1561 (efl_arg_0_4 ?i)))) )) (ite (is-IfThenElse!1567 (efl_arg_0_4 ?i)) (and (not (forall ((?z I_efl)) (not (= (efl_arg_0_4 ?z) (then!1569 (efl_arg_0_4 ?i)))) )) (not (forall ((?z I_efl)) (not (= (efl_arg_0_4 ?z) (elze!1570 (efl_arg_0_4 ?i)))) ))) (ite (is-While!1575 (efl_arg_0_4 ?i)) (not (forall ((?z I_efl)) (not (= (efl_arg_0_4 ?z) (body!1577 (efl_arg_0_4 ?i)))) )) (ite (is-For!1562 (efl_arg_0_4 ?i)) (and (not (forall ((?z I_efl)) (not (= (efl_arg_0_4 ?z) (init!1563 (efl_arg_0_4 ?i)))) )) (not (forall ((?z I_efl)) (not (= (efl_arg_0_4 ?z) (body!1566 (efl_arg_0_4 ?i)))) )) (not (forall ((?z I_efl)) (not (= (efl_arg_0_4 ?z) (step!1565 (efl_arg_0_4 ?i)))) ))) true))))) )) +(assert (exists ((stat!216 Statement!1556)) (not (=> (and (and (and (and (is-For!1562 stat!216) (is-For!1562 stat!216)) (and (ifree (ite (is-Block!1560 (init!1563 stat!216)) (Block!1560 (efll (body!1561 (init!1563 stat!216)))) (ite (is-IfThenElse!1567 (init!1563 stat!216)) (IfThenElse!1567 (expr!1568 (init!1563 stat!216)) (efl (then!1569 (init!1563 stat!216))) (efl (elze!1570 (init!1563 stat!216)))) (ite (is-While!1575 (init!1563 stat!216)) (While!1575 (expr!1576 (init!1563 stat!216)) (efl (body!1577 (init!1563 stat!216)))) (ite (is-For!1562 (init!1563 stat!216)) (Block!1560 (Cons!1618 (efl (init!1563 (init!1563 stat!216))) (Cons!1618 (While!1575 (expr!1564 (init!1563 stat!216)) (Block!1560 (Cons!1618 (efl (body!1566 (init!1563 stat!216))) (Cons!1618 (efl (step!1565 (init!1563 stat!216))) Nil!1621)))) Nil!1621))) (init!1563 stat!216)))))) (not (forall ((?z I_ifree)) (not (= (ifree_arg_0_1 ?z) (ite (is-Block!1560 (init!1563 stat!216)) (Block!1560 (efll (body!1561 (init!1563 stat!216)))) (ite (is-IfThenElse!1567 (init!1563 stat!216)) (IfThenElse!1567 (expr!1568 (init!1563 stat!216)) (efl (then!1569 (init!1563 stat!216))) (efl (elze!1570 (init!1563 stat!216)))) (ite (is-While!1575 (init!1563 stat!216)) (While!1575 (expr!1576 (init!1563 stat!216)) (efl (body!1577 (init!1563 stat!216)))) (ite (is-For!1562 (init!1563 stat!216)) (Block!1560 (Cons!1618 (efl (init!1563 (init!1563 stat!216))) (Cons!1618 (While!1575 (expr!1564 (init!1563 stat!216)) (Block!1560 (Cons!1618 (efl (body!1566 (init!1563 stat!216))) (Cons!1618 (efl (step!1565 (init!1563 stat!216))) Nil!1621)))) Nil!1621))) (init!1563 stat!216))))))) )) (ite (is-Block!1560 (init!1563 stat!216)) (not (forall ((?z I_efll)) (not (= (efll_arg_0_3 ?z) (body!1561 (init!1563 stat!216)))) )) (ite (is-IfThenElse!1567 (init!1563 stat!216)) (and (not (forall ((?z I_efl)) (not (= (efl_arg_0_4 ?z) (then!1569 (init!1563 stat!216)))) )) (not (forall ((?z I_efl)) (not (= (efl_arg_0_4 ?z) (elze!1570 (init!1563 stat!216)))) ))) (ite (is-While!1575 (init!1563 stat!216)) (not (forall ((?z I_efl)) (not (= (efl_arg_0_4 ?z) (body!1577 (init!1563 stat!216)))) )) (ite (is-For!1562 (init!1563 stat!216)) (and (not (forall ((?z I_efl)) (not (= (efl_arg_0_4 ?z) (init!1563 (init!1563 stat!216)))) )) (not (forall ((?z I_efl)) (not (= (efl_arg_0_4 ?z) (body!1566 (init!1563 stat!216)))) )) (not (forall ((?z I_efl)) (not (= (efl_arg_0_4 ?z) (step!1565 (init!1563 stat!216)))) ))) true)))))) (and (ifree (ite (is-Block!1560 (step!1565 stat!216)) (Block!1560 (efll (body!1561 (step!1565 stat!216)))) (ite (is-IfThenElse!1567 (step!1565 stat!216)) (IfThenElse!1567 (expr!1568 (step!1565 stat!216)) (efl (then!1569 (step!1565 stat!216))) (efl (elze!1570 (step!1565 stat!216)))) (ite (is-While!1575 (step!1565 stat!216)) (While!1575 (expr!1576 (step!1565 stat!216)) (efl (body!1577 (step!1565 stat!216)))) (ite (is-For!1562 (step!1565 stat!216)) (Block!1560 (Cons!1618 (efl (init!1563 (step!1565 stat!216))) (Cons!1618 (While!1575 (expr!1564 (step!1565 stat!216)) (Block!1560 (Cons!1618 (efl (body!1566 (step!1565 stat!216))) (Cons!1618 (efl (step!1565 (step!1565 stat!216))) Nil!1621)))) Nil!1621))) (step!1565 stat!216)))))) (not (forall ((?z I_ifree)) (not (= (ifree_arg_0_1 ?z) (ite (is-Block!1560 (step!1565 stat!216)) (Block!1560 (efll (body!1561 (step!1565 stat!216)))) (ite (is-IfThenElse!1567 (step!1565 stat!216)) (IfThenElse!1567 (expr!1568 (step!1565 stat!216)) (efl (then!1569 (step!1565 stat!216))) (efl (elze!1570 (step!1565 stat!216)))) (ite (is-While!1575 (step!1565 stat!216)) (While!1575 (expr!1576 (step!1565 stat!216)) (efl (body!1577 (step!1565 stat!216)))) (ite (is-For!1562 (step!1565 stat!216)) (Block!1560 (Cons!1618 (efl (init!1563 (step!1565 stat!216))) (Cons!1618 (While!1575 (expr!1564 (step!1565 stat!216)) (Block!1560 (Cons!1618 (efl (body!1566 (step!1565 stat!216))) (Cons!1618 (efl (step!1565 (step!1565 stat!216))) Nil!1621)))) Nil!1621))) (step!1565 stat!216))))))) )) (ite (is-Block!1560 (step!1565 stat!216)) (not (forall ((?z I_efll)) (not (= (efll_arg_0_3 ?z) (body!1561 (step!1565 stat!216)))) )) (ite (is-IfThenElse!1567 (step!1565 stat!216)) (and (not (forall ((?z I_efl)) (not (= (efl_arg_0_4 ?z) (then!1569 (step!1565 stat!216)))) )) (not (forall ((?z I_efl)) (not (= (efl_arg_0_4 ?z) (elze!1570 (step!1565 stat!216)))) ))) (ite (is-While!1575 (step!1565 stat!216)) (not (forall ((?z I_efl)) (not (= (efl_arg_0_4 ?z) (body!1577 (step!1565 stat!216)))) )) (ite (is-For!1562 (step!1565 stat!216)) (and (not (forall ((?z I_efl)) (not (= (efl_arg_0_4 ?z) (init!1563 (step!1565 stat!216)))) )) (not (forall ((?z I_efl)) (not (= (efl_arg_0_4 ?z) (body!1566 (step!1565 stat!216)))) )) (not (forall ((?z I_efl)) (not (= (efl_arg_0_4 ?z) (step!1565 (step!1565 stat!216)))) ))) true)))))) (and (ifree (ite (is-Block!1560 (body!1566 stat!216)) (Block!1560 (efll (body!1561 (body!1566 stat!216)))) (ite (is-IfThenElse!1567 (body!1566 stat!216)) (IfThenElse!1567 (expr!1568 (body!1566 stat!216)) (efl (then!1569 (body!1566 stat!216))) (efl (elze!1570 (body!1566 stat!216)))) (ite (is-While!1575 (body!1566 stat!216)) (While!1575 (expr!1576 (body!1566 stat!216)) (efl (body!1577 (body!1566 stat!216)))) (ite (is-For!1562 (body!1566 stat!216)) (Block!1560 (Cons!1618 (efl (init!1563 (body!1566 stat!216))) (Cons!1618 (While!1575 (expr!1564 (body!1566 stat!216)) (Block!1560 (Cons!1618 (efl (body!1566 (body!1566 stat!216))) (Cons!1618 (efl (step!1565 (body!1566 stat!216))) Nil!1621)))) Nil!1621))) (body!1566 stat!216)))))) (not (forall ((?z I_ifree)) (not (= (ifree_arg_0_1 ?z) (ite (is-Block!1560 (body!1566 stat!216)) (Block!1560 (efll (body!1561 (body!1566 stat!216)))) (ite (is-IfThenElse!1567 (body!1566 stat!216)) (IfThenElse!1567 (expr!1568 (body!1566 stat!216)) (efl (then!1569 (body!1566 stat!216))) (efl (elze!1570 (body!1566 stat!216)))) (ite (is-While!1575 (body!1566 stat!216)) (While!1575 (expr!1576 (body!1566 stat!216)) (efl (body!1577 (body!1566 stat!216)))) (ite (is-For!1562 (body!1566 stat!216)) (Block!1560 (Cons!1618 (efl (init!1563 (body!1566 stat!216))) (Cons!1618 (While!1575 (expr!1564 (body!1566 stat!216)) (Block!1560 (Cons!1618 (efl (body!1566 (body!1566 stat!216))) (Cons!1618 (efl (step!1565 (body!1566 stat!216))) Nil!1621)))) Nil!1621))) (body!1566 stat!216))))))) )) (ite (is-Block!1560 (body!1566 stat!216)) (not (forall ((?z I_efll)) (not (= (efll_arg_0_3 ?z) (body!1561 (body!1566 stat!216)))) )) (ite (is-IfThenElse!1567 (body!1566 stat!216)) (and (not (forall ((?z I_efl)) (not (= (efl_arg_0_4 ?z) (then!1569 (body!1566 stat!216)))) )) (not (forall ((?z I_efl)) (not (= (efl_arg_0_4 ?z) (elze!1570 (body!1566 stat!216)))) ))) (ite (is-While!1575 (body!1566 stat!216)) (not (forall ((?z I_efl)) (not (= (efl_arg_0_4 ?z) (body!1577 (body!1566 stat!216)))) )) (ite (is-For!1562 (body!1566 stat!216)) (and (not (forall ((?z I_efl)) (not (= (efl_arg_0_4 ?z) (init!1563 (body!1566 stat!216)))) )) (not (forall ((?z I_efl)) (not (= (efl_arg_0_4 ?z) (body!1566 (body!1566 stat!216)))) )) (not (forall ((?z I_efl)) (not (= (efl_arg_0_4 ?z) (step!1565 (body!1566 stat!216)))) ))) true)))))) (or (ifree (ite (is-Block!1560 stat!216) (Block!1560 (efll (body!1561 stat!216))) (ite (is-IfThenElse!1567 stat!216) (IfThenElse!1567 (expr!1568 stat!216) (efl (then!1569 stat!216)) (efl (elze!1570 stat!216))) (ite (is-While!1575 stat!216) (While!1575 (expr!1576 stat!216) (efl (body!1577 stat!216))) (ite (is-For!1562 stat!216) (Block!1560 (Cons!1618 (efl (init!1563 stat!216)) (Cons!1618 (While!1575 (expr!1564 stat!216) (Block!1560 (Cons!1618 (efl (body!1566 stat!216)) (Cons!1618 (efl (step!1565 stat!216)) Nil!1621)))) Nil!1621))) stat!216))))) (forall ((?z I_ifree)) (not (= (ifree_arg_0_1 ?z) (ite (is-Block!1560 stat!216) (Block!1560 (efll (body!1561 stat!216))) (ite (is-IfThenElse!1567 stat!216) (IfThenElse!1567 (expr!1568 stat!216) (efl (then!1569 stat!216)) (efl (elze!1570 stat!216))) (ite (is-While!1575 stat!216) (While!1575 (expr!1576 stat!216) (efl (body!1577 stat!216))) (ite (is-For!1562 stat!216) (Block!1560 (Cons!1618 (efl (init!1563 stat!216)) (Cons!1618 (While!1575 (expr!1564 stat!216) (Block!1560 (Cons!1618 (efl (body!1566 stat!216)) (Cons!1618 (efl (step!1565 stat!216)) Nil!1621)))) Nil!1621))) stat!216)))))) ) (not (ite (is-Block!1560 stat!216) (not (forall ((?z I_efll)) (not (= (efll_arg_0_3 ?z) (body!1561 stat!216))) )) (ite (is-IfThenElse!1567 stat!216) (and (not (forall ((?z I_efl)) (not (= (efl_arg_0_4 ?z) (then!1569 stat!216))) )) (not (forall ((?z I_efl)) (not (= (efl_arg_0_4 ?z) (elze!1570 stat!216))) ))) (ite (is-While!1575 stat!216) (not (forall ((?z I_efl)) (not (= (efl_arg_0_4 ?z) (body!1577 stat!216))) )) (ite (is-For!1562 stat!216) (and (not (forall ((?z I_efl)) (not (= (efl_arg_0_4 ?z) (init!1563 stat!216))) )) (not (forall ((?z I_efl)) (not (= (efl_arg_0_4 ?z) (body!1566 stat!216))) )) (not (forall ((?z I_efl)) (not (= (efl_arg_0_4 ?z) (step!1565 stat!216))) ))) true)))))))) )) +(check-sat) diff --git a/test/regress/regress0/fmf/LeftistHeap.scala-8-ncm.smt2 b/test/regress/regress0/fmf/LeftistHeap.scala-8-ncm.smt2 new file mode 100644 index 000000000..9ef5f14fa --- /dev/null +++ b/test/regress/regress0/fmf/LeftistHeap.scala-8-ncm.smt2 @@ -0,0 +1,33 @@ +; COMMAND-LINE: --finite-model-find +; EXPECT: sat +(set-logic ALL_SUPPORTED) +(set-info :status sat) +(declare-datatypes () ((array!896 (array!896!897 (size!898 (_ BitVec 32)) (content!899 (Array (_ BitVec 32) (_ BitVec 32))))))) +(declare-datatypes () ((tuple2!900 (tuple2!900!901 (_1!902 array!896) (_2!903 (_ BitVec 32)))))) +(declare-fun error_value!904 () (_ BitVec 32)) +(declare-fun error_value!905 () (_ BitVec 32)) +(declare-fun error_value!906 () array!896) +(declare-fun error_value!907 () (_ BitVec 32)) +(declare-fun error_value!908 () array!896) +(declare-fun error_value!909 () (_ BitVec 32)) +(declare-fun while0!216 (array!896 (_ BitVec 32) array!896) tuple2!900) +(declare-fun isPositive!206 (array!896 (_ BitVec 32)) Bool) +(declare-fun rec!210 ((_ BitVec 32) array!896 (_ BitVec 32)) Bool) +(declare-fun arrayconst!910 () (Array (_ BitVec 32) (_ BitVec 32))) +(declare-sort I_while0!216 0) +(declare-fun while0!216_arg_0_1 (I_while0!216) array!896) +(declare-fun while0!216_arg_1_2 (I_while0!216) (_ BitVec 32)) +(declare-fun while0!216_arg_2_3 (I_while0!216) array!896) +(declare-sort I_isPositive!206 0) +(declare-fun isPositive!206_arg_0_4 (I_isPositive!206) array!896) +(declare-fun isPositive!206_arg_1_5 (I_isPositive!206) (_ BitVec 32)) +(declare-sort I_rec!210 0) +(declare-fun rec!210_arg_0_6 (I_rec!210) (_ BitVec 32)) +(declare-fun rec!210_arg_1_7 (I_rec!210) array!896) +(declare-fun rec!210_arg_2_8 (I_rec!210) (_ BitVec 32)) +(assert (forall ((?i I_while0!216)) (and (= (while0!216 (while0!216_arg_0_1 ?i) (while0!216_arg_1_2 ?i) (while0!216_arg_2_3 ?i)) (ite (bvslt (while0!216_arg_1_2 ?i) (size!898 (while0!216_arg_2_3 ?i))) (while0!216 (ite (bvslt (ite (and (bvslt (while0!216_arg_1_2 ?i) (size!898 (while0!216_arg_2_3 ?i))) (not (bvslt (while0!216_arg_1_2 ?i) (_ bv0 32)))) (select (content!899 (while0!216_arg_2_3 ?i)) (while0!216_arg_1_2 ?i)) error_value!904) (_ bv0 32)) (ite (and (bvslt (while0!216_arg_1_2 ?i) (size!898 (while0!216_arg_0_1 ?i))) (not (bvslt (while0!216_arg_1_2 ?i) (_ bv0 32)))) (array!896!897 (size!898 (while0!216_arg_0_1 ?i)) (store (content!899 (while0!216_arg_0_1 ?i)) (while0!216_arg_1_2 ?i) (bvneg (ite (and (bvslt (while0!216_arg_1_2 ?i) (size!898 (while0!216_arg_2_3 ?i))) (not (bvslt (while0!216_arg_1_2 ?i) (_ bv0 32)))) (select (content!899 (while0!216_arg_2_3 ?i)) (while0!216_arg_1_2 ?i)) error_value!905)))) error_value!906) (ite (and (bvslt (while0!216_arg_1_2 ?i) (size!898 (while0!216_arg_0_1 ?i))) (not (bvslt (while0!216_arg_1_2 ?i) (_ bv0 32)))) (array!896!897 (size!898 (while0!216_arg_0_1 ?i)) (store (content!899 (while0!216_arg_0_1 ?i)) (while0!216_arg_1_2 ?i) (ite (and (bvslt (while0!216_arg_1_2 ?i) (size!898 (while0!216_arg_2_3 ?i))) (not (bvslt (while0!216_arg_1_2 ?i) (_ bv0 32)))) (select (content!899 (while0!216_arg_2_3 ?i)) (while0!216_arg_1_2 ?i)) error_value!907))) error_value!908)) (bvadd (while0!216_arg_1_2 ?i) (_ bv1 32)) (while0!216_arg_2_3 ?i)) (tuple2!900!901 (while0!216_arg_0_1 ?i) (while0!216_arg_1_2 ?i)))) (ite (bvslt (while0!216_arg_1_2 ?i) (size!898 (while0!216_arg_2_3 ?i))) (not (forall ((?z I_while0!216)) (not (and (= (while0!216_arg_0_1 ?z) (ite (bvslt (ite (and (bvslt (while0!216_arg_1_2 ?i) (size!898 (while0!216_arg_2_3 ?i))) (not (bvslt (while0!216_arg_1_2 ?i) (_ bv0 32)))) (select (content!899 (while0!216_arg_2_3 ?i)) (while0!216_arg_1_2 ?i)) error_value!904) (_ bv0 32)) (ite (and (bvslt (while0!216_arg_1_2 ?i) (size!898 (while0!216_arg_0_1 ?i))) (not (bvslt (while0!216_arg_1_2 ?i) (_ bv0 32)))) (array!896!897 (size!898 (while0!216_arg_0_1 ?i)) (store (content!899 (while0!216_arg_0_1 ?i)) (while0!216_arg_1_2 ?i) (bvneg (ite (and (bvslt (while0!216_arg_1_2 ?i) (size!898 (while0!216_arg_2_3 ?i))) (not (bvslt (while0!216_arg_1_2 ?i) (_ bv0 32)))) (select (content!899 (while0!216_arg_2_3 ?i)) (while0!216_arg_1_2 ?i)) error_value!905)))) error_value!906) (ite (and (bvslt (while0!216_arg_1_2 ?i) (size!898 (while0!216_arg_0_1 ?i))) (not (bvslt (while0!216_arg_1_2 ?i) (_ bv0 32)))) (array!896!897 (size!898 (while0!216_arg_0_1 ?i)) (store (content!899 (while0!216_arg_0_1 ?i)) (while0!216_arg_1_2 ?i) (ite (and (bvslt (while0!216_arg_1_2 ?i) (size!898 (while0!216_arg_2_3 ?i))) (not (bvslt (while0!216_arg_1_2 ?i) (_ bv0 32)))) (select (content!899 (while0!216_arg_2_3 ?i)) (while0!216_arg_1_2 ?i)) error_value!907))) error_value!908))) (= (while0!216_arg_1_2 ?z) (bvadd (while0!216_arg_1_2 ?i) (_ bv1 32))) (= (while0!216_arg_2_3 ?z) (while0!216_arg_2_3 ?i)))) )) true)) )) +(assert (forall ((?i I_isPositive!206)) (and (= (isPositive!206 (isPositive!206_arg_0_4 ?i) (isPositive!206_arg_1_5 ?i)) (rec!210 (_ bv0 32) (isPositive!206_arg_0_4 ?i) (isPositive!206_arg_1_5 ?i))) (not (forall ((?z I_rec!210)) (not (and (= (rec!210_arg_0_6 ?z) (_ bv0 32)) (= (rec!210_arg_1_7 ?z) (isPositive!206_arg_0_4 ?i)) (= (rec!210_arg_2_8 ?z) (isPositive!206_arg_1_5 ?i)))) ))) )) +(assert (forall ((?i I_rec!210)) (and (= (rec!210 (rec!210_arg_0_6 ?i) (rec!210_arg_1_7 ?i) (rec!210_arg_2_8 ?i)) (ite (not (bvslt (rec!210_arg_0_6 ?i) (rec!210_arg_2_8 ?i))) true (ite (bvslt (ite (and (bvslt (rec!210_arg_0_6 ?i) (size!898 (rec!210_arg_1_7 ?i))) (not (bvslt (rec!210_arg_0_6 ?i) (_ bv0 32)))) (select (content!899 (rec!210_arg_1_7 ?i)) (rec!210_arg_0_6 ?i)) error_value!909) (_ bv0 32)) false (rec!210 (bvadd (rec!210_arg_0_6 ?i) (_ bv1 32)) (rec!210_arg_1_7 ?i) (rec!210_arg_2_8 ?i))))) (ite (not (bvslt (rec!210_arg_0_6 ?i) (rec!210_arg_2_8 ?i))) true (ite (bvslt (ite (and (bvslt (rec!210_arg_0_6 ?i) (size!898 (rec!210_arg_1_7 ?i))) (not (bvslt (rec!210_arg_0_6 ?i) (_ bv0 32)))) (select (content!899 (rec!210_arg_1_7 ?i)) (rec!210_arg_0_6 ?i)) error_value!909) (_ bv0 32)) true (not (forall ((?z I_rec!210)) (not (and (= (rec!210_arg_0_6 ?z) (bvadd (rec!210_arg_0_6 ?i) (_ bv1 32))) (= (rec!210_arg_1_7 ?z) (rec!210_arg_1_7 ?i)) (= (rec!210_arg_2_8 ?z) (rec!210_arg_2_8 ?i)))) ))))) )) +(assert (not (forall ((tab!211 array!896)) (or (or (bvslt (size!898 (_1!902 (while0!216 (array!896!897 (size!898 tab!211) arrayconst!910) (_ bv0 32) tab!211))) (_ bv0 32)) (forall ((?z I_while0!216)) (not (and (= (while0!216_arg_0_1 ?z) (array!896!897 (size!898 tab!211) arrayconst!910)) (= (while0!216_arg_1_2 ?z) (_ bv0 32)) (= (while0!216_arg_2_3 ?z) tab!211))) )) (or (isPositive!206 (_1!902 (while0!216 (array!896!897 (size!898 tab!211) arrayconst!910) (_ bv0 32) tab!211)) (size!898 tab!211)) (forall ((?z I_isPositive!206)) (not (and (= (isPositive!206_arg_0_4 ?z) (_1!902 (while0!216 (array!896!897 (size!898 tab!211) arrayconst!910) (_ bv0 32) tab!211))) (= (isPositive!206_arg_1_5 ?z) (size!898 tab!211)))) ) (forall ((?z I_while0!216)) (not (and (= (while0!216_arg_0_1 ?z) (array!896!897 (size!898 tab!211) arrayconst!910)) (= (while0!216_arg_1_2 ?z) (_ bv0 32)) (= (while0!216_arg_2_3 ?z) tab!211))) ))) ))) +(check-sat) + diff --git a/test/regress/regress0/fmf/Makefile.am b/test/regress/regress0/fmf/Makefile.am index 8cff980a5..575aa4159 100644 --- a/test/regress/regress0/fmf/Makefile.am +++ b/test/regress/regress0/fmf/Makefile.am @@ -50,8 +50,12 @@ TESTS = \ loopy_coda.smt2 \ fmc_unsound_model.smt2 \ am-bad-model.cvc \ - nun-0208-to.smt2 - + nun-0208-to.smt2 \ + datatypes-ufinite.smt2 \ + datatypes-ufinite-nested.smt2 \ + ForElimination-scala-9.smt2 \ + agree466.smt2 \ + LeftistHeap.scala-8-ncm.smt2 EXTRA_DIST = $(TESTS) @@ -66,7 +70,6 @@ EXTRA_DIST = $(TESTS) #EXTRA_DIST += \ # error.cvc -# agree466.smt2 timeout after commit on 1/14 due to Array+FMF model construction # synonyms for "check" in this directory .PHONY: regress regress0 test diff --git a/test/regress/regress0/fmf/datatypes-ufinite-nested.smt2 b/test/regress/regress0/fmf/datatypes-ufinite-nested.smt2 new file mode 100644 index 000000000..3ffc36d05 --- /dev/null +++ b/test/regress/regress0/fmf/datatypes-ufinite-nested.smt2 @@ -0,0 +1,17 @@ +; COMMAND-LINE: --finite-model-find +; EXPECT: sat +(set-logic ALL_SUPPORTED) +(declare-sort U 0) +(declare-fun a () U) +(declare-fun b () U) +(declare-fun c () U) +(declare-fun d () U) +(assert (distinct a b c)) +(declare-sort V 0) +(declare-datatypes () ((ufin1 (cons1 (s11 U) (s13 ufin2))) (ufin2 (cons2 (s21 V) (s22 U)) (cons3)))) +(declare-fun P (ufin1 ufin2) Bool) +(declare-fun Q (ufin1 ufin1) Bool) +(assert (forall ((x ufin1) (y ufin2) (z ufin1)) (or (P x y) (Q x z)))) +(assert (not (P (cons1 a cons3) cons3))) +(assert (not (Q (cons1 b cons3) (cons1 a cons3)))) +(check-sat) diff --git a/test/regress/regress0/fmf/datatypes-ufinite.smt2 b/test/regress/regress0/fmf/datatypes-ufinite.smt2 new file mode 100644 index 000000000..3564bff8b --- /dev/null +++ b/test/regress/regress0/fmf/datatypes-ufinite.smt2 @@ -0,0 +1,17 @@ +; COMMAND-LINE: --finite-model-find +; EXPECT: sat +(set-logic ALL_SUPPORTED) +(declare-sort U 0) +(declare-fun a () U) +(declare-fun b () U) +(declare-fun c () U) +(declare-fun d () U) +(assert (distinct a b c)) +(declare-sort V 0) +(declare-datatypes () ((ufin1 (cons1 (s11 U) (s12 U))) (ufin2 (cons2 (s21 V) (s22 U)) (cons3)))) +(declare-fun P (ufin1 ufin2) Bool) +(declare-fun Q (ufin1 ufin1) Bool) +(assert (forall ((x ufin1) (y ufin2) (z ufin1)) (or (P x y) (Q x z)))) +(assert (not (P (cons1 a a) cons3))) +(assert (not (Q (cons1 a d) (cons1 a b)))) +(check-sat) diff --git a/test/regress/regress0/push-pop/Makefile.am b/test/regress/regress0/push-pop/Makefile.am index bcf6403b7..4bc16ea25 100644 --- a/test/regress/regress0/push-pop/Makefile.am +++ b/test/regress/regress0/push-pop/Makefile.am @@ -44,7 +44,8 @@ BUG_TESTS = \ bug-fmf-fun-skolem.smt2 \ bug674.smt2 \ inc-double-u.smt2 \ - fmf-fun-dbu.smt2 + fmf-fun-dbu.smt2 \ + inc-define.smt2 TESTS = $(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(BUG_TESTS) diff --git a/test/regress/regress0/push-pop/inc-define.smt2 b/test/regress/regress0/push-pop/inc-define.smt2 new file mode 100644 index 000000000..27261eff6 --- /dev/null +++ b/test/regress/regress0/push-pop/inc-define.smt2 @@ -0,0 +1,9 @@ +; COMMAND-LINE: --incremental +; EXPECT: sat +; EXPECT: sat +(set-logic QF_LIA) +(declare-fun x () Int) +(check-sat) +(define t (not (= x 0))) +(assert t) +(check-sat) diff --git a/test/regress/regress0/quantifiers/Makefile.am b/test/regress/regress0/quantifiers/Makefile.am index df146752e..6b5e0d1ed 100644 --- a/test/regress/regress0/quantifiers/Makefile.am +++ b/test/regress/regress0/quantifiers/Makefile.am @@ -38,10 +38,9 @@ TESTS = \ gauss_init_0030.fof.smt2 \ qcft-javafe.filespace.TreeWalker.006.smt2 \ qcft-smtlib3dbc51.smt2 \ - symmetric_unsat_7.smt2 \ javafe.ast.StmtVec.009.smt2 \ ARI176e1.smt2 \ - bi-artm-s.smt2 \ + bi-artm-s.smt2 \ simp-typ-test.smt2 \ macros-int-real.smt2 \ stream-x2014-09-18-unsat.smt2 \ @@ -65,12 +64,22 @@ TESTS = \ ext-ex-deq-trigger.smt2 \ matching-lia-1arg.smt2 \ RND_4_16.smt2 \ - cdt-0208-to.smt2 \ - psyco-196.smt2 \ - agg-rew-test.smt2 \ - agg-rew-test-cf.smt2 \ - rew-to-0211-dd.smt2 \ - rew-to-scala.smt2 + cdt-0208-to.smt2 \ + psyco-196.smt2 \ + agg-rew-test.smt2 \ + agg-rew-test-cf.smt2 \ + rew-to-0211-dd.smt2 \ + rew-to-scala.smt2 \ + macro-subtype-param.smt2 \ + macros-real-arg.smt2 \ + subtype-param-unk.smt2 \ + subtype-param.smt2 \ + anti-sk-simp.smt2 \ + pure_dt_cbqi.smt2 \ + florian-case-ax.smt2 \ + double-pattern.smt2 \ + qcf-rel-dom-opt.smt2 \ + parametric-lists.smt2 # regression can be solved with --finite-model-find --fmf-inst-engine diff --git a/test/regress/regress0/quantifiers/anti-sk-simp.smt2 b/test/regress/regress0/quantifiers/anti-sk-simp.smt2 new file mode 100755 index 000000000..ba4f9cbb9 --- /dev/null +++ b/test/regress/regress0/quantifiers/anti-sk-simp.smt2 @@ -0,0 +1,10 @@ +; COMMAND-LINE: --quant-anti-skolem +; EXPECT: unsat +(set-logic ALL_SUPPORTED) +(set-info :status unsat) +(declare-fun f (Int) Int) +(declare-fun a () Int) +(declare-fun b () Int) +(assert (forall ((X Int)) (< X (f X)))) +(assert (forall ((X Int)) (> (+ a b) (f X)))) +(check-sat) diff --git a/test/regress/regress0/quantifiers/double-pattern.smt2 b/test/regress/regress0/quantifiers/double-pattern.smt2 new file mode 100644 index 000000000..4ce21d446 --- /dev/null +++ b/test/regress/regress0/quantifiers/double-pattern.smt2 @@ -0,0 +1,6 @@ +(set-logic UFLIA) +(set-info :status unsat) +(declare-fun P (Int) Bool) +(assert (forall ((x Int)) (! (! (P x) :pattern ((P x))) :pattern ((P x))))) +(assert (not (P 0))) +(check-sat) diff --git a/test/regress/regress0/quantifiers/florian-case-ax.smt2 b/test/regress/regress0/quantifiers/florian-case-ax.smt2 new file mode 100644 index 000000000..35ebb28e9 --- /dev/null +++ b/test/regress/regress0/quantifiers/florian-case-ax.smt2 @@ -0,0 +1,168 @@ +(set-logic AUFLIA) +(set-info :status unsat) +(declare-sort U 0) +(declare-fun A (U U U + U U U U + U U U U + U U U U + U U U U + U U U U + U U U U + U U U U + U U U U + U U U U + U U U U + U U U U + U U U U + U U U U + U U + U) (Array Int U)) + +(assert + (forall ((v_184 U) (v_185 U) + (v_186 U) (v_187 U) + (v_188 U) (v_189 U) + (v_190 U) (v_191 U) + (v_192 U) (v_193 U) + (v_194 U) (v_195 U) + (v_196 U) (v_197 U) + (v_198 U) (v_199 U) + (v_200 U) (v_201 U) + (v_202 U) (v_203 U) + (v_204 U) (v_205 U) + (v_206 U) (v_207 U) + (v_208 U) (v_209 U) + (v_210 U) (v_211 U) + (v_212 U) (v_213 U) + (v_214 U) (v_215 U) + (v_216 U) (v_217 U) + (v_218 U) (v_219 U) + (v_220 U) (v_221 U) + (v_222 U) (v_223 U) + (v_224 U) (v_225 U) + (v_226 U) (v_227 U) + (v_228 U) (v_229 U) + (v_230 U) (v_231 U) + (v_232 U) (v_233 U) + (v_234 U) (v_235 U) + (v_236 U) (v_237 U) + (v_238 U) (v_239 U) + (v_240 U) (v_241 U) (v_242 Int)) + (let ((v_183 (A v_184 v_185 v_186 v_187 + v_188 v_189 v_190 v_191 v_192 + v_193 v_194 v_195 v_196 v_197 + v_198 v_199 v_200 v_201 v_202 + v_203 v_204 v_205 v_206 v_207 + v_208 v_209 v_210 v_211 v_212 + v_213 v_214 v_215 v_216 v_217 + v_218 v_219 v_220 v_221 v_222 + v_223 v_224 v_225 v_226 v_227 + v_228 v_229 v_230 v_231 v_232 + v_233 v_234 v_235 v_236 v_237 + v_238 v_239 v_240 v_241))) + (ite (= v_242 59) (= (select v_183 v_242) v_240) + (ite (= v_242 58) (= (select v_183 v_242) v_239) + (ite (= v_242 57) (= (select v_183 v_242) v_238) + (ite (= v_242 56) (= (select v_183 v_242) v_237) + (ite (= v_242 55) (= (select v_183 v_242) v_236) + (ite (= v_242 54) (= (select v_183 v_242) v_235) + (ite (= v_242 53) (= (select v_183 v_242) v_234) + (ite (= v_242 52) (= (select v_183 v_242) v_233) + (ite (= v_242 51) (= (select v_183 v_242) v_232) + (ite (= v_242 50) (= (select v_183 v_242) v_231) + (ite (= v_242 49) (= (select v_183 v_242) v_230) + (ite (= v_242 48) (= (select v_183 v_242) v_229) + (ite (= v_242 47) (= (select v_183 v_242) v_228) + (ite (= v_242 46) (= (select v_183 v_242) v_227) + (ite (= v_242 45) (= (select v_183 v_242) v_226) + (ite (= v_242 44) (= (select v_183 v_242) v_225) + (ite (= v_242 43) (= (select v_183 v_242) v_224) + (ite (= v_242 41) (= (select v_183 v_242) v_223) + (ite (= v_242 40) (= (select v_183 v_242) v_222) + (ite (= v_242 39) (= (select v_183 v_242) v_221) + (ite (= v_242 37) (= (select v_183 v_242) v_220) + (ite (= v_242 36) (= (select v_183 v_242) v_219) + (ite (= v_242 34) (= (select v_183 v_242) v_218) + (ite (= v_242 33) (= (select v_183 v_242) v_217) + (ite (= v_242 32) (= (select v_183 v_242) v_216) + (ite (= v_242 31) (= (select v_183 v_242) v_215) + (ite (= v_242 30) (= (select v_183 v_242) v_214) + (ite (= v_242 29) (= (select v_183 v_242) v_213) + (ite (= v_242 28) (= (select v_183 v_242) v_212) + (ite (= v_242 27) (= (select v_183 v_242) v_211) + (ite (= v_242 26) (= (select v_183 v_242) v_210) + (ite (= v_242 25) (= (select v_183 v_242) v_209) + (ite (= v_242 24) (= (select v_183 v_242) v_208) + (ite (= v_242 23) (= (select v_183 v_242) v_207) + (ite (= v_242 22) (= (select v_183 v_242) v_206) + (ite (= v_242 21) (= (select v_183 v_242) v_205) + (ite (= v_242 20) (= (select v_183 v_242) v_204) + (ite (= v_242 19) (= (select v_183 v_242) v_203) + (ite (= v_242 18) (= (select v_183 v_242) v_202) + (ite (= v_242 17) (= (select v_183 v_242) v_201) + (ite (= v_242 16) (= (select v_183 v_242) v_200) + (ite (= v_242 15) (= (select v_183 v_242) v_199) + (ite (= v_242 14) (= (select v_183 v_242) v_198) + (ite (= v_242 13) (= (select v_183 v_242) v_197) + (ite (= v_242 12) (= (select v_183 v_242) v_196) + (ite (= v_242 11) (= (select v_183 v_242) v_195) + (ite (= v_242 10) (= (select v_183 v_242) v_194) + (ite (= v_242 9) (= (select v_183 v_242) v_193) + (ite (= v_242 8) (= (select v_183 v_242) v_192) + (ite (= v_242 7) (= (select v_183 v_242) v_191) + (ite (= v_242 6) (= (select v_183 v_242) v_190) + (ite (= v_242 5) (= (select v_183 v_242) v_189) + (ite (= v_242 4) (= (select v_183 v_242) v_188) + (ite (= v_242 3) (= (select v_183 v_242) v_187) + (ite (= v_242 2) (= (select v_183 v_242) v_186) + (ite (= v_242 1) (= (select v_183 v_242) v_185) + (ite (= v_242 0) (= (select v_183 v_242) v_184) + (= (select v_183 v_242) v_241))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) + +(declare-const c_184 U) (declare-const c_185 U) +(declare-const c_186 U) (declare-const c_187 U) +(declare-const c_188 U) (declare-const c_189 U) +(declare-const c_190 U) (declare-const c_191 U) +(declare-const c_192 U) (declare-const c_193 U) +(declare-const c_194 U) (declare-const c_195 U) +(declare-const c_196 U) (declare-const c_197 U) +(declare-const c_198 U) (declare-const c_199 U) +(declare-const c_200 U) (declare-const c_201 U) +(declare-const c_202 U) (declare-const c_203 U) +(declare-const c_204 U) (declare-const c_205 U) +(declare-const c_206 U) (declare-const c_207 U) +(declare-const c_208 U) (declare-const c_209 U) +(declare-const c_210 U) (declare-const c_211 U) +(declare-const c_212 U) (declare-const c_213 U) +(declare-const c_214 U) (declare-const c_215 U) +(declare-const c_216 U) (declare-const c_217 U) +(declare-const c_218 U) (declare-const c_219 U) +(declare-const c_220 U) (declare-const c_221 U) +(declare-const c_222 U) (declare-const c_223 U) +(declare-const c_224 U) (declare-const c_225 U) +(declare-const c_226 U) (declare-const c_227 U) +(declare-const c_228 U) (declare-const c_229 U) +(declare-const c_230 U) (declare-const c_231 U) +(declare-const c_232 U) (declare-const c_233 U) +(declare-const c_234 U) (declare-const c_235 U) +(declare-const c_236 U) (declare-const c_237 U) +(declare-const c_238 U) (declare-const c_239 U) +(declare-const c_240 U) (declare-const c_241 U) + +(declare-fun b () Int) +(declare-fun c () U) +(assert (not (= (select (A c_184 c_185 c_186 c_187 + c_188 c_189 c_190 c_191 c_192 + c_193 c_194 c_195 c_196 c_197 + c_198 c_199 c_200 c_201 c_202 + c_203 c_204 c_205 c_206 c_207 + c_208 c_209 c_210 c_211 c_212 + c_213 c_214 c_215 c_216 c_217 + c_218 c_219 c_220 c_221 c_222 + c_223 c_224 c_225 c_226 c_227 + c_228 c_229 c_230 c_231 c_232 + c_233 c_234 c_235 c_236 c_237 + c_238 c_239 c_240 c_241) b) c))) +(assert (and (= b 28) (= c c_212))) + +(check-sat) diff --git a/test/regress/regress0/quantifiers/macro-subtype-param.smt2 b/test/regress/regress0/quantifiers/macro-subtype-param.smt2 new file mode 100644 index 000000000..20de79047 --- /dev/null +++ b/test/regress/regress0/quantifiers/macro-subtype-param.smt2 @@ -0,0 +1,18 @@ +; COMMAND-LINE: --macros-quant +; EXPECT: unknown +; this will fail if type rule for APPLY_UF requires to be subtypes +(set-logic ALL_SUPPORTED) + +(declare-datatypes (T) ((List (cons (hd T) (tl (List T))) (nil)))) + +(declare-fun R ((List Int)) Bool) +(assert (forall ((x (List Int))) (R x))) +(declare-fun j1 () (List Real)) +(assert (not (R j1))) + +(declare-fun Q ((Array Real Int)) Bool) +(assert (forall ((x (Array Real Int))) (Q x))) +(declare-fun j2 () (Array Int Real)) +(assert (not (Q j2))) + +(check-sat) diff --git a/test/regress/regress0/quantifiers/macros-real-arg.smt2 b/test/regress/regress0/quantifiers/macros-real-arg.smt2 new file mode 100644 index 000000000..675c96d68 --- /dev/null +++ b/test/regress/regress0/quantifiers/macros-real-arg.smt2 @@ -0,0 +1,11 @@ +; COMMAND-LINE: --macros-quant +; EXPECT: unsat +; this will fail if type rule for APPLY_UF is made strict +(set-logic UFLIRA) +(declare-fun P (Int) Bool) +(assert (forall ((x Int)) (P x))) +(declare-fun k () Real) +(declare-fun k2 () Int) +(assert (or (not (P k)) (not (P k2)))) +(assert (= k 0)) +(check-sat) diff --git a/test/regress/regress0/quantifiers/parametric-lists.smt2 b/test/regress/regress0/quantifiers/parametric-lists.smt2 new file mode 100644 index 000000000..c117934f8 --- /dev/null +++ b/test/regress/regress0/quantifiers/parametric-lists.smt2 @@ -0,0 +1,42 @@ +(set-logic ALL_SUPPORTED) +(set-info :status unsat) +(declare-datatypes (T) ((List (cons (head T) (tail (List T))) (nil)))) +(declare-datatypes () ((KV (kv (key Int) (value Int)) (nilKV)))) ; key value pair +(declare-fun mapper ((List Int)) (List KV)) +(assert + (forall + ((input (List Int))) + (ite + (= input (as nil (List Int))) + (= (as nil (List KV)) (mapper input)) + (= (cons (kv 0 (head input)) (mapper (tail input))) (mapper input)) + ) + ) +) +(declare-fun reduce ((List KV)) Int) +(assert + (forall + ((inputk (List KV))) + (ite + (= inputk (as nil (List KV))) + (= 0 (reduce inputk)) + (= (+ (value (head inputk)) (reduce (tail inputk))) (reduce inputk)) + ) + ) +) +(declare-fun sum ((List Int)) Int) +(assert + (forall + ((input (List Int))) + (ite + (= input (as nil (List Int))) + (= 0 (sum input)) + (= (+ (head input) (sum (tail input))) (sum input)) + ) + ) +) +(assert + (not (= (sum (cons 0 (as nil (List Int)))) (reduce (mapper (cons 0 (as nil (List Int))))))) +) +(check-sat) + diff --git a/test/regress/regress0/quantifiers/pure_dt_cbqi.smt2 b/test/regress/regress0/quantifiers/pure_dt_cbqi.smt2 new file mode 100644 index 000000000..a11d14e4a --- /dev/null +++ b/test/regress/regress0/quantifiers/pure_dt_cbqi.smt2 @@ -0,0 +1,6 @@ +(set-logic ALL_SUPPORTED)
+(set-info :status sat)
+(declare-datatypes () ((nat (Suc (pred nat)) (zero))))
+(declare-fun y () nat)
+(assert (forall ((x nat)) (not (= y (Suc x)))))
+(check-sat)
diff --git a/test/regress/regress0/quantifiers/qcf-rel-dom-opt.smt2 b/test/regress/regress0/quantifiers/qcf-rel-dom-opt.smt2 new file mode 100644 index 000000000..539f181af --- /dev/null +++ b/test/regress/regress0/quantifiers/qcf-rel-dom-opt.smt2 @@ -0,0 +1,45 @@ +(set-logic UFLIA) +(set-info :status unsat) +(declare-fun P (Int) Bool) + +(assert (P 0)) +(assert (P 1)) +(assert (P 2)) +(assert (P 3)) +(assert (P 4)) +(assert (P 5)) +(assert (P 6)) +(assert (P 7)) +(assert (P 8)) +(assert (P 9)) + +(assert (P 10)) +(assert (P 11)) +(assert (P 12)) +(assert (P 13)) +(assert (P 14)) +(assert (P 15)) +(assert (P 16)) +(assert (P 17)) +(assert (P 18)) +(assert (P 19)) + +(assert (P 20)) +(assert (P 21)) +(assert (P 22)) +(assert (P 23)) +(assert (P 24)) +(assert (P 25)) +(assert (P 26)) +(assert (P 27)) +(assert (P 28)) +(assert (P 29)) + +(declare-fun Q (Int Int Int Int Int) Bool) +(assert (forall ((x Int) (y Int) (z Int) (w Int) (q Int)) (or (not (P x)) (not (P y)) (not (P z)) (not (P w)) (not (P q)) (Q x y z w q)))) + +(declare-fun R (Int) Bool) +(assert (R 0)) +(assert (forall ((x Int)) (not (R x)))) + +(check-sat) diff --git a/test/regress/regress0/quantifiers/subtype-param-unk.smt2 b/test/regress/regress0/quantifiers/subtype-param-unk.smt2 new file mode 100644 index 000000000..836449cb9 --- /dev/null +++ b/test/regress/regress0/quantifiers/subtype-param-unk.smt2 @@ -0,0 +1,19 @@ +; COMMAND-LINE: +; EXPECT: unknown +; this will fail if type rule for APPLY_UF requires arguments to be subtypes +(set-logic ALL_SUPPORTED) + +(declare-datatypes (T) ((List (cons (hd T) (tl (List T))) (nil)))) + +(declare-fun R ((List Int)) Bool) + +(assert (forall ((x (List Int))) (R x))) +(declare-fun j1 () (List Real)) +(assert (not (R j1))) + +(declare-fun Q ((Array Int Real)) Bool) +(assert (forall ((x (Array Int Int))) (Q x))) +(declare-fun j2 () (Array Int Real)) +(assert (not (Q j2))) + +(check-sat) diff --git a/test/regress/regress0/quantifiers/subtype-param.smt2 b/test/regress/regress0/quantifiers/subtype-param.smt2 new file mode 100644 index 000000000..08615abf6 --- /dev/null +++ b/test/regress/regress0/quantifiers/subtype-param.smt2 @@ -0,0 +1,16 @@ +(set-logic ALL_SUPPORTED) +(set-info :status unsat) + +(declare-datatypes (T) ((List (cons (hd T) (tl (List T))) (nil)))) + +(declare-fun R ((List Int)) Bool) +(assert (forall ((x (List Real))) (R x))) + +(declare-fun Q ((Array Int Real)) Bool) +(assert (forall ((x (Array Int Int))) (Q x))) + +(declare-fun k1 () (List Int)) +(declare-fun k2 () (Array Real Int)) +(assert (or (not (R k1)) (not (Q k2)))) + +(check-sat) diff --git a/test/regress/regress0/sets/card-2.smt2 b/test/regress/regress0/sets/card-2.smt2 new file mode 100644 index 000000000..cb414dbef --- /dev/null +++ b/test/regress/regress0/sets/card-2.smt2 @@ -0,0 +1,10 @@ +(set-logic QF_UFLIAFS) +(declare-sort E 0) +(declare-fun s () (Set E)) +(declare-fun t () (Set E)) +(declare-fun u () (Set E)) +(assert (>= (card s) 5)) +(assert (>= (card t) 5)) +(assert (<= (card u) 6)) +(assert (= u (union s t))) +(check-sat) diff --git a/test/regress/regress0/sets/card-3.smt2 b/test/regress/regress0/sets/card-3.smt2 new file mode 100644 index 000000000..949ed3457 --- /dev/null +++ b/test/regress/regress0/sets/card-3.smt2 @@ -0,0 +1,11 @@ +(set-logic QF_UFLIAFS) +(declare-sort E 0) +(declare-fun s () (Set E)) +(declare-fun t () (Set E)) +(declare-fun u () (Set E)) +(assert (>= (card (union s t)) 8)) +(assert (>= (card (union s u)) 8)) +(assert (<= (card (union t u)) 5)) +(assert (<= (card s) 5)) +(assert (= (as emptyset (Set E)) (intersection t u))) +(check-sat) diff --git a/test/regress/regress0/sets/card-4.smt2 b/test/regress/regress0/sets/card-4.smt2 new file mode 100644 index 000000000..ea7fe42f3 --- /dev/null +++ b/test/regress/regress0/sets/card-4.smt2 @@ -0,0 +1,23 @@ +(set-logic QF_UFLIAFS) +(declare-sort E 0) +(declare-fun s () (Set E)) +(declare-fun t () (Set E)) +(declare-fun u () (Set E)) +(assert (>= (card (union s t)) 8)) +(assert (>= (card (union s u)) 8)) +;(assert (<= (card (union t u)) 5)) +(assert (<= (card s) 5)) +(assert (= (as emptyset (Set E)) (intersection t u))) +(declare-fun x1 () E) +(declare-fun x2 () E) +(declare-fun x3 () E) +(declare-fun x4 () E) +(declare-fun x5 () E) +(declare-fun x6 () E) +(assert (member x1 s)) +(assert (member x2 s)) +(assert (member x3 s)) +(assert (member x4 s)) +(assert (member x5 s)) +(assert (member x6 s)) +(check-sat) diff --git a/test/regress/regress0/sets/card-5.smt2 b/test/regress/regress0/sets/card-5.smt2 new file mode 100644 index 000000000..65135e7b4 --- /dev/null +++ b/test/regress/regress0/sets/card-5.smt2 @@ -0,0 +1,24 @@ +(set-logic QF_UFLIAFS) +(declare-sort E 0) +(declare-fun s () (Set E)) +(declare-fun t () (Set E)) +(declare-fun u () (Set E)) +(assert (>= (card (union s t)) 8)) +(assert (>= (card (union s u)) 8)) +;(assert (<= (card (union t u)) 5)) +(assert (<= (card s) 5)) +(assert (= (as emptyset (Set E)) (intersection t u))) +(declare-fun x1 () E) +(declare-fun x2 () E) +(declare-fun x3 () E) +(declare-fun x4 () E) +(declare-fun x5 () E) +(declare-fun x6 () E) +(assert (member x1 s)) +(assert (member x2 s)) +(assert (member x3 s)) +(assert (member x4 s)) +(assert (member x5 s)) +(assert (member x6 s)) +(assert (distinct x1 x2 x3 x4 x5 x6)) +(check-sat) diff --git a/test/regress/regress0/sets/card-6.smt2 b/test/regress/regress0/sets/card-6.smt2 new file mode 100644 index 000000000..1611952b7 --- /dev/null +++ b/test/regress/regress0/sets/card-6.smt2 @@ -0,0 +1,16 @@ +(set-logic QF_UFLIAFS) +(declare-sort E 0) +(declare-fun A () (Set E)) +(declare-fun B () (Set E)) +(declare-fun C () (Set E)) +(assert + (and + (= (as emptyset (Set E)) + (intersection A B)) + (subset C (union A B)) + (>= (card C) 5) + (<= (card A) 2) + (<= (card B) 2) + ) +) +(check-sat) diff --git a/test/regress/regress0/sets/card-7.smt2 b/test/regress/regress0/sets/card-7.smt2 new file mode 100644 index 000000000..94468dc57 --- /dev/null +++ b/test/regress/regress0/sets/card-7.smt2 @@ -0,0 +1,46 @@ +(set-logic QF_UFLIAFS) +(declare-sort E 0) +(declare-fun A1 () (Set E)) +(declare-fun A2 () (Set E)) +(declare-fun A3 () (Set E)) +(declare-fun A4 () (Set E)) +(declare-fun A5 () (Set E)) +(declare-fun A6 () (Set E)) +(declare-fun A7 () (Set E)) +(declare-fun A8 () (Set E)) +(declare-fun A9 () (Set E)) +(declare-fun A10 () (Set E)) +(declare-fun A11 () (Set E)) +(declare-fun A12 () (Set E)) +(declare-fun A13 () (Set E)) +(declare-fun A14 () (Set E)) +(declare-fun A15 () (Set E)) +(declare-fun A16 () (Set E)) +(declare-fun A17 () (Set E)) +(declare-fun A18 () (Set E)) +(declare-fun A19 () (Set E)) +(declare-fun A20 () (Set E)) +(assert (and + (= (card A1) 1) + (= (card A2) 1) + (= (card A3) 1) + (= (card A4) 1) + (= (card A5) 1) + (= (card A6) 1) + (= (card A7) 1) + (= (card A8) 1) + (= (card A9) 1) + (= (card A10) 1) + (= (card A11) 1) + (= (card A12) 1) + (= (card A13) 1) + (= (card A14) 1) + (= (card A15) 1) + (= (card A16) 1) + (= (card A17) 1) + (= (card A18) 1) + (= (card A19) 1) + (= (card A20) 1) +)) +(assert (= 20 (+ (card A1) (card A2) (card A3) (card A4) (card A5) (card A6) (card A7) (card A8) (card A9) (card A10) (card A11) (card A12) (card A13) (card A14) (card A15) (card A16) (card A17) (card A18) (card A19) (card A20)))) +(check-sat) diff --git a/test/regress/regress0/sets/card.smt2 b/test/regress/regress0/sets/card.smt2 new file mode 100644 index 000000000..6b8c536d5 --- /dev/null +++ b/test/regress/regress0/sets/card.smt2 @@ -0,0 +1,8 @@ +(set-logic QF_UFLIAFS) +(declare-sort E 0) +(declare-fun s () (Set E)) +(declare-fun t () (Set E)) +(assert (>= (card s) 5)) +(assert (>= (card t) 5)) +(assert (<= (card (union s t)) 4)) +(check-sat) diff --git a/test/regress/regress0/strings/Makefile.am b/test/regress/regress0/strings/Makefile.am index f5c6048e6..771b9f031 100644 --- a/test/regress/regress0/strings/Makefile.am +++ b/test/regress/regress0/strings/Makefile.am @@ -74,7 +74,9 @@ TESTS = \ idof-handg.smt2 \ fmf001.smt2 \ type002.smt2 \ - crash-1019.smt2 + crash-1019.smt2 \ + norn-31.smt2 \ + strings-native-simple.cvc FAILING_TESTS = diff --git a/test/regress/regress0/strings/norn-31.smt2 b/test/regress/regress0/strings/norn-31.smt2 new file mode 100644 index 000000000..4698f966f --- /dev/null +++ b/test/regress/regress0/strings/norn-31.smt2 @@ -0,0 +1,23 @@ +(set-logic QF_SLIA) +(set-option :strings-exp true) +(set-info :status unsat) + +(declare-fun var_0 () String) +(declare-fun var_1 () String) +(declare-fun var_2 () String) +(declare-fun var_3 () String) +(declare-fun var_4 () String) +(declare-fun var_5 () String) +(declare-fun var_6 () String) +(declare-fun var_7 () String) +(declare-fun var_8 () String) +(declare-fun var_9 () String) +(declare-fun var_10 () String) +(declare-fun var_11 () String) +(declare-fun var_12 () String) + +(assert (str.in.re var_1 (re.* (re.range "a" "u")))) +(assert (str.in.re var_1 (re.++ (re.* (str.to.re "a")) (str.to.re "b")))) +(assert (str.in.re var_1 (re.++ (re.++ (re.++ (re.* (re.union (str.to.re "a") (str.to.re "b"))) (str.to.re "b")) (str.to.re "a")) (re.* (re.union (str.to.re "a") (str.to.re "b")))))) +(assert (not (str.in.re "" re.nostr))) +(check-sat) diff --git a/test/regress/regress0/strings/strings-native-simple.cvc b/test/regress/regress0/strings/strings-native-simple.cvc new file mode 100644 index 000000000..568452e12 --- /dev/null +++ b/test/regress/regress0/strings/strings-native-simple.cvc @@ -0,0 +1,10 @@ +% EXPECT: sat + +x : STRING; +y : STRING; + +ASSERT x = CONCAT( "abcd", y ); +ASSERT LENGTH( x ) >= 6; +ASSERT LENGTH( y ) < 5; + +CHECKSAT; diff --git a/test/regress/regress0/sygus/Makefile.am b/test/regress/regress0/sygus/Makefile.am index 32caa4989..2ca807662 100644 --- a/test/regress/regress0/sygus/Makefile.am +++ b/test/regress/regress0/sygus/Makefile.am @@ -47,7 +47,8 @@ TESTS = commutative.sy \ list-head-x.sy \ clock-inc-tuple.sy \ dt-test-ns.sy \ - no-mention.sy + no-mention.sy \ + max2-univ.sy # sygus tests currently taking too long for make regress EXTRA_DIST = $(TESTS) \ diff --git a/test/regress/regress0/sygus/max2-univ.sy b/test/regress/regress0/sygus/max2-univ.sy new file mode 100644 index 000000000..3f8aac3b2 --- /dev/null +++ b/test/regress/regress0/sygus/max2-univ.sy @@ -0,0 +1,12 @@ +; EXPECT: unsat +; COMMAND-LINE: --cegqi --no-dump-synth +; Synthesize the maximum of 2 integers, but property has 4 variables (requires 2 passes) +(set-logic LIA) +(synth-fun max2 ((x Int) (y Int)) Int) +(declare-var x Int) +(declare-var y Int) +(declare-var r Int) +(declare-var w Int) +(constraint (=> (< r 0) (=> (or (and (= x w) (= y (+ w r))) (and (= x (+ w r)) (= y w))) (= (max2 x y) w)))) +(check-synth) + diff --git a/test/system/CVC4JavaTest.java b/test/system/CVC4JavaTest.java index 902af6c26..bd0d1ff65 100644 --- a/test/system/CVC4JavaTest.java +++ b/test/system/CVC4JavaTest.java @@ -1,13 +1,13 @@ /********************* */ /*! \file CVC4JavaTest.java ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: none - ** Minor contributors (to current version): none + ** Top contributors (to current version): + ** Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim ** ** \brief [[ Add one-line brief description here ]] ** diff --git a/test/system/boilerplate.cpp b/test/system/boilerplate.cpp index 8d5f3b795..297f69a4f 100644 --- a/test/system/boilerplate.cpp +++ b/test/system/boilerplate.cpp @@ -1,13 +1,13 @@ /********************* */ /*! \file boilerplate.cpp ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: none - ** Minor contributors (to current version): Tim King + ** Top contributors (to current version): + ** Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim ** ** \brief A simple start-up/tear-down test for CVC4. ** diff --git a/test/system/cvc3_george.cpp b/test/system/cvc3_george.cpp index 267211ded..bf7650a55 100644 --- a/test/system/cvc3_george.cpp +++ b/test/system/cvc3_george.cpp @@ -1,13 +1,13 @@ /********************* */ /*! \file cvc3_george.cpp ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: none - ** Minor contributors (to current version): none + ** Top contributors (to current version): + ** Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim ** ** \brief Test of CVC3 compatibility interface ** diff --git a/test/system/cvc3_george.h b/test/system/cvc3_george.h index 86b53008e..9dba3ed61 100644 --- a/test/system/cvc3_george.h +++ b/test/system/cvc3_george.h @@ -1,13 +1,13 @@ /********************* */ /*! \file cvc3_george.h ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: none - ** Minor contributors (to current version): none + ** Top contributors (to current version): + ** Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim ** ** \brief Test of CVC3 compatibility interface ** diff --git a/test/system/cvc3_main.cpp b/test/system/cvc3_main.cpp index ada82a80f..c74cb7355 100644 --- a/test/system/cvc3_main.cpp +++ b/test/system/cvc3_main.cpp @@ -1,13 +1,13 @@ /********************* */ /*! \file cvc3_main.cpp ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: none - ** Minor contributors (to current version): none + ** Top contributors (to current version): + ** Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim ** ** \brief Test of CVC3 compatibility interface ** diff --git a/test/system/ouroborous.cpp b/test/system/ouroborous.cpp index 1ceb7319f..189bf20cd 100644 --- a/test/system/ouroborous.cpp +++ b/test/system/ouroborous.cpp @@ -1,13 +1,13 @@ /********************* */ /*! \file ouroborous.cpp ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: none - ** Minor contributors (to current version): none + ** Top contributors (to current version): + ** Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim ** ** \brief "Ouroborous" test: does CVC4 read its own output? ** diff --git a/test/system/smt2_compliance.cpp b/test/system/smt2_compliance.cpp index 68fbb9f59..933f8c6cd 100644 --- a/test/system/smt2_compliance.cpp +++ b/test/system/smt2_compliance.cpp @@ -1,13 +1,13 @@ /********************* */ /*! \file smt2_compliance.cpp ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: none - ** Minor contributors (to current version): none + ** Top contributors (to current version): + ** Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim ** ** \brief A test of SMT-LIBv2 commands, checks for compliant output ** diff --git a/test/system/statistics.cpp b/test/system/statistics.cpp index 18b1e5937..11b8cd3ee 100644 --- a/test/system/statistics.cpp +++ b/test/system/statistics.cpp @@ -1,13 +1,13 @@ /********************* */ /*! \file statistics.cpp ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: none - ** Minor contributors (to current version): none + ** Top contributors (to current version): + ** Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim ** ** \brief A simple statistics test for CVC4. ** diff --git a/test/system/two_smt_engines.cpp b/test/system/two_smt_engines.cpp index eb56aeebf..c916ac711 100644 --- a/test/system/two_smt_engines.cpp +++ b/test/system/two_smt_engines.cpp @@ -1,13 +1,13 @@ /********************* */ /*! \file two_smt_engines.cpp ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: none - ** Minor contributors (to current version): none + ** Top contributors (to current version): + ** Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim ** ** \brief A simple test of multiple SmtEngines ** diff --git a/test/unit/context/cdlist_black.h b/test/unit/context/cdlist_black.h index 5980972be..8929e8fb4 100644 --- a/test/unit/context/cdlist_black.h +++ b/test/unit/context/cdlist_black.h @@ -1,13 +1,13 @@ /********************* */ /*! \file cdlist_black.h ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: none - ** Minor contributors (to current version): Tim King + ** Top contributors (to current version): + ** Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim ** ** \brief Black box testing of CVC4::context::CDList<>. ** diff --git a/test/unit/context/cdlist_context_memory_black.h b/test/unit/context/cdlist_context_memory_black.h index 359c3dce5..a43d34b00 100644 --- a/test/unit/context/cdlist_context_memory_black.h +++ b/test/unit/context/cdlist_context_memory_black.h @@ -1,13 +1,13 @@ /********************* */ /*! \file cdlist_context_memory_black.h ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: Tim King - ** Minor contributors (to current version): none + ** Top contributors (to current version): + ** Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim ** ** \brief Black box testing of CVC4::context::CDList<>. ** diff --git a/test/unit/context/cdmap_black.h b/test/unit/context/cdmap_black.h index aad5c49d0..3da4dc0b0 100644 --- a/test/unit/context/cdmap_black.h +++ b/test/unit/context/cdmap_black.h @@ -1,13 +1,13 @@ /********************* */ /*! \file cdmap_black.h ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: none - ** Minor contributors (to current version): Tim King, Dejan Jovanovic + ** Top contributors (to current version): + ** Morgan Deters, Tim King, Dejan Jovanovic ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim ** ** \brief Black box testing of CVC4::context::CDMap<>. ** diff --git a/test/unit/context/cdmap_white.h b/test/unit/context/cdmap_white.h index 11642c3e9..ec071125b 100644 --- a/test/unit/context/cdmap_white.h +++ b/test/unit/context/cdmap_white.h @@ -1,13 +1,13 @@ /********************* */ /*! \file cdmap_white.h ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: none - ** Minor contributors (to current version): Dejan Jovanovic + ** Top contributors (to current version): + ** Morgan Deters, Tim King, Dejan Jovanovic ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim ** ** \brief White box testing of CVC4::context::CDMap<>. ** diff --git a/test/unit/context/cdo_black.h b/test/unit/context/cdo_black.h index 4ca01df85..c88f79f76 100644 --- a/test/unit/context/cdo_black.h +++ b/test/unit/context/cdo_black.h @@ -1,13 +1,13 @@ /********************* */ /*! \file cdo_black.h ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: none - ** Minor contributors (to current version): none + ** Top contributors (to current version): + ** Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim ** ** \brief Black box testing of CVC4::context::CDO<>. ** diff --git a/test/unit/context/cdvector_black.h b/test/unit/context/cdvector_black.h index c2a5259ee..4b47c0660 100644 --- a/test/unit/context/cdvector_black.h +++ b/test/unit/context/cdvector_black.h @@ -1,13 +1,13 @@ /********************* */ /*! \file cdvector_black.h ** \verbatim - ** Original author: Tim King - ** Major contributors: none - ** Minor contributors (to current version): Morgan Deters + ** Top contributors (to current version): + ** Tim King, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim ** ** \brief [[ Add one-line brief description here ]] ** diff --git a/test/unit/context/context_black.h b/test/unit/context/context_black.h index d7148c990..e8bb6beb2 100644 --- a/test/unit/context/context_black.h +++ b/test/unit/context/context_black.h @@ -1,13 +1,13 @@ /********************* */ /*! \file context_black.h ** \verbatim - ** Original author: Dejan Jovanovic - ** Major contributors: Morgan Deters - ** Minor contributors (to current version): none + ** Top contributors (to current version): + ** Morgan Deters, Dejan Jovanovic, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim ** ** \brief Black box testing of CVC4::context::Context. ** diff --git a/test/unit/context/context_mm_black.h b/test/unit/context/context_mm_black.h index e58b22895..60671653c 100644 --- a/test/unit/context/context_mm_black.h +++ b/test/unit/context/context_mm_black.h @@ -1,13 +1,13 @@ /********************* */ /*! \file context_mm_black.h ** \verbatim - ** Original author: Dejan Jovanovic - ** Major contributors: Morgan Deters - ** Minor contributors (to current version): none + ** Top contributors (to current version): + ** Dejan Jovanovic, Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim ** ** \brief Black box testing of CVC4::context::ContextMemoryManager. ** diff --git a/test/unit/context/context_white.h b/test/unit/context/context_white.h index 10f603abd..8dfc8a29a 100644 --- a/test/unit/context/context_white.h +++ b/test/unit/context/context_white.h @@ -1,13 +1,13 @@ /********************* */ /*! \file context_white.h ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: none - ** Minor contributors (to current version): none + ** Top contributors (to current version): + ** Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim ** ** \brief White box testing of CVC4::context::Context. ** diff --git a/test/unit/context/stacking_vector_black.h b/test/unit/context/stacking_vector_black.h index 35305e469..ef85c86b4 100644 --- a/test/unit/context/stacking_vector_black.h +++ b/test/unit/context/stacking_vector_black.h @@ -1,13 +1,13 @@ /********************* */ /*! \file stacking_vector_black.h ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: none - ** Minor contributors (to current version): none + ** Top contributors (to current version): + ** Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim ** ** \brief Black box testing of CVC4::context::StackingVector ** diff --git a/test/unit/expr/attribute_black.h b/test/unit/expr/attribute_black.h index bea04a139..b02827680 100644 --- a/test/unit/expr/attribute_black.h +++ b/test/unit/expr/attribute_black.h @@ -1,13 +1,13 @@ /********************* */ /*! \file attribute_black.h ** \verbatim - ** Original author: Dejan Jovanovic - ** Major contributors: Morgan Deters, Tim King - ** Minor contributors (to current version): Christopher L. Conway + ** Top contributors (to current version): + ** Tim King, Dejan Jovanovic, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim ** ** \brief Black box testing of CVC4::Attribute. ** diff --git a/test/unit/expr/attribute_white.h b/test/unit/expr/attribute_white.h index df7e263d2..1db44f097 100644 --- a/test/unit/expr/attribute_white.h +++ b/test/unit/expr/attribute_white.h @@ -1,13 +1,13 @@ /********************* */ /*! \file attribute_white.h ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: none - ** Minor contributors (to current version): Dejan Jovanovic, Christopher L. Conway + ** Top contributors (to current version): + ** Morgan Deters, Christopher L. Conway, Dejan Jovanovic ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim ** ** \brief White box testing of Node attributes. ** diff --git a/test/unit/expr/expr_manager_public.h b/test/unit/expr/expr_manager_public.h index 17efaf2a5..788b4964b 100644 --- a/test/unit/expr/expr_manager_public.h +++ b/test/unit/expr/expr_manager_public.h @@ -1,13 +1,13 @@ /********************* */ /*! \file expr_manager_public.h ** \verbatim - ** Original author: Christopher L. Conway - ** Major contributors: none - ** Minor contributors (to current version): Tim King, Morgan Deters + ** Top contributors (to current version): + ** Christopher L. Conway, Tim King, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim ** ** \brief Public black-box testing of CVC4::ExprManager. ** diff --git a/test/unit/expr/expr_public.h b/test/unit/expr/expr_public.h index 194aec0b1..ed772a471 100644 --- a/test/unit/expr/expr_public.h +++ b/test/unit/expr/expr_public.h @@ -1,13 +1,13 @@ /********************* */ /*! \file expr_public.h ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: Christopher L. Conway, Dejan Jovanovic - ** Minor contributors (to current version): Tim King, Clark Barrett + ** Top contributors (to current version): + ** Morgan Deters, Dejan Jovanovic, Christopher L. Conway ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim ** ** \brief Public black-box testing of CVC4::Expr. ** @@ -58,7 +58,7 @@ public: char *argv[2]; argv[0] = strdup(""); argv[1] = strdup("--output-language=ast"); - opts.parseOptions(2, argv); + Options::parseOptions(&opts, 2, argv); free(argv[0]); free(argv[1]); diff --git a/test/unit/expr/kind_black.h b/test/unit/expr/kind_black.h index 9deb8ce71..fd53a4e0a 100644 --- a/test/unit/expr/kind_black.h +++ b/test/unit/expr/kind_black.h @@ -1,13 +1,13 @@ /********************* */ /*! \file kind_black.h ** \verbatim - ** Original author: Tim King - ** Major contributors: none - ** Minor contributors (to current version): Morgan Deters + ** Top contributors (to current version): + ** Tim King, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim ** ** \brief Black box testing of CVC4::Kind. ** diff --git a/test/unit/expr/kind_map_black.h b/test/unit/expr/kind_map_black.h index 489aaaa21..0e34be366 100644 --- a/test/unit/expr/kind_map_black.h +++ b/test/unit/expr/kind_map_black.h @@ -1,13 +1,13 @@ /********************* */ /*! \file kind_map_black.h ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: none - ** Minor contributors (to current version): none + ** Top contributors (to current version): + ** Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim ** ** \brief Black box testing of CVC4::KindMap ** diff --git a/test/unit/expr/node_black.h b/test/unit/expr/node_black.h index 7d6ee523a..1f190b73d 100644 --- a/test/unit/expr/node_black.h +++ b/test/unit/expr/node_black.h @@ -1,13 +1,13 @@ /********************* */ /*! \file node_black.h ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: Tim King - ** Minor contributors (to current version): Christopher L. Conway, Dejan Jovanovic + ** Top contributors (to current version): + ** Morgan Deters, Tim King, Dejan Jovanovic ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim ** ** \brief Black box testing of CVC4::Node. ** @@ -45,7 +45,7 @@ public: char *argv[2]; argv[0] = strdup(""); argv[1] = strdup("--output-language=ast"); - opts.parseOptions(2, argv); + Options::parseOptions(&opts, 2, argv); free(argv[0]); free(argv[1]); diff --git a/test/unit/expr/node_builder_black.h b/test/unit/expr/node_builder_black.h index a7ebea2fe..c21abbd75 100644 --- a/test/unit/expr/node_builder_black.h +++ b/test/unit/expr/node_builder_black.h @@ -1,13 +1,13 @@ /********************* */ /*! \file node_builder_black.h ** \verbatim - ** Original author: Tim King - ** Major contributors: Christopher L. Conway, Morgan Deters - ** Minor contributors (to current version): Dejan Jovanovic + ** Top contributors (to current version): + ** Tim King, Morgan Deters, Christopher L. Conway ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim ** ** \brief Black box testing of CVC4::NodeBuilder. ** diff --git a/test/unit/expr/node_manager_black.h b/test/unit/expr/node_manager_black.h index 781829e36..3958e0f2c 100644 --- a/test/unit/expr/node_manager_black.h +++ b/test/unit/expr/node_manager_black.h @@ -1,13 +1,13 @@ /********************* */ /*! \file node_manager_black.h ** \verbatim - ** Original author: Christopher L. Conway - ** Major contributors: Morgan Deters, Dejan Jovanovic - ** Minor contributors (to current version): Tim King + ** Top contributors (to current version): + ** Christopher L. Conway, Dejan Jovanovic, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim ** ** \brief White box testing of CVC4::NodeManager. ** diff --git a/test/unit/expr/node_manager_white.h b/test/unit/expr/node_manager_white.h index fa44b837a..2bda4d2f0 100644 --- a/test/unit/expr/node_manager_white.h +++ b/test/unit/expr/node_manager_white.h @@ -1,13 +1,13 @@ /********************* */ /*! \file node_manager_white.h ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: none - ** Minor contributors (to current version): Tim King + ** Top contributors (to current version): + ** Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim ** ** \brief White box testing of CVC4::NodeManager. ** diff --git a/test/unit/expr/node_self_iterator_black.h b/test/unit/expr/node_self_iterator_black.h index 7240deed5..a55a79da0 100644 --- a/test/unit/expr/node_self_iterator_black.h +++ b/test/unit/expr/node_self_iterator_black.h @@ -1,13 +1,13 @@ /********************* */ /*! \file node_self_iterator_black.h ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: none - ** Minor contributors (to current version): none + ** Top contributors (to current version): + ** Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim ** ** \brief Black box testing of CVC4::expr::NodeSelfIterator ** diff --git a/test/unit/expr/node_white.h b/test/unit/expr/node_white.h index 594a981c8..0be08f588 100644 --- a/test/unit/expr/node_white.h +++ b/test/unit/expr/node_white.h @@ -1,13 +1,13 @@ /********************* */ /*! \file node_white.h ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: none - ** Minor contributors (to current version): Tim King, Dejan Jovanovic + ** Top contributors (to current version): + ** Morgan Deters, Tim King, Dejan Jovanovic ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim ** ** \brief White box testing of CVC4::Node. ** diff --git a/test/unit/expr/symbol_table_black.h b/test/unit/expr/symbol_table_black.h index 2b26ad745..f6c476288 100644 --- a/test/unit/expr/symbol_table_black.h +++ b/test/unit/expr/symbol_table_black.h @@ -1,13 +1,13 @@ /********************* */ /*! \file symbol_table_black.h ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: Christopher L. Conway - ** Minor contributors (to current version): Dejan Jovanovic + ** Top contributors (to current version): + ** Christopher L. Conway, Morgan Deters, Dejan Jovanovic ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim ** ** \brief Black box testing of CVC4::SymbolTable ** diff --git a/test/unit/expr/type_cardinality_public.h b/test/unit/expr/type_cardinality_public.h index 8eb59952a..dd2578e06 100644 --- a/test/unit/expr/type_cardinality_public.h +++ b/test/unit/expr/type_cardinality_public.h @@ -1,13 +1,13 @@ /********************* */ /*! \file type_cardinality_public.h ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: none - ** Minor contributors (to current version): none + ** Top contributors (to current version): + ** Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim ** ** \brief Public box testing of Type::getCardinality() for various Types ** diff --git a/test/unit/expr/type_node_white.h b/test/unit/expr/type_node_white.h index ce1ce1534..77c0c721b 100644 --- a/test/unit/expr/type_node_white.h +++ b/test/unit/expr/type_node_white.h @@ -1,13 +1,13 @@ /********************* */ /*! \file type_node_white.h ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: none - ** Minor contributors (to current version): none + ** Top contributors (to current version): + ** Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim ** ** \brief White box testing of TypeNode ** diff --git a/test/unit/main/interactive_shell_black.h b/test/unit/main/interactive_shell_black.h index b351f5c3e..f1fce3cb8 100644 --- a/test/unit/main/interactive_shell_black.h +++ b/test/unit/main/interactive_shell_black.h @@ -1,13 +1,13 @@ /********************* */ /*! \file interactive_shell_black.h ** \verbatim - ** Original author: Christopher L. Conway - ** Major contributors: none - ** Minor contributors (to current version): Morgan Deters + ** Top contributors (to current version): + ** Christopher L. Conway, Tim King, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim ** ** \brief Black box testing of CVC4::InteractiveShell. ** diff --git a/test/unit/memory.h b/test/unit/memory.h index 06c4a4a44..73e4814e7 100644 --- a/test/unit/memory.h +++ b/test/unit/memory.h @@ -1,13 +1,13 @@ /********************* */ /*! \file memory.h ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: none - ** Minor contributors (to current version): none + ** Top contributors (to current version): + ** Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim ** ** \brief Utility class to help testing out-of-memory conditions. ** diff --git a/test/unit/parser/parser_black.h b/test/unit/parser/parser_black.h index 3c4171925..595280491 100644 --- a/test/unit/parser/parser_black.h +++ b/test/unit/parser/parser_black.h @@ -1,13 +1,13 @@ /********************* */ /*! \file parser_black.h ** \verbatim - ** Original author: Christopher L. Conway - ** Major contributors: Morgan Deters - ** Minor contributors (to current version): none + ** Top contributors (to current version): + ** Christopher L. Conway, Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim ** ** \brief Black box testing of CVC4::parser::Parser, including CVC, SMT and ** SMT v2 inputs. diff --git a/test/unit/parser/parser_builder_black.h b/test/unit/parser/parser_builder_black.h index 42d240668..42ebc2cf9 100644 --- a/test/unit/parser/parser_builder_black.h +++ b/test/unit/parser/parser_builder_black.h @@ -1,13 +1,13 @@ /********************* */ /*! \file parser_builder_black.h ** \verbatim - ** Original author: Christopher L. Conway - ** Major contributors: none - ** Minor contributors (to current version): Morgan Deters + ** Top contributors (to current version): + ** Christopher L. Conway, Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim ** ** \brief Black box testing of CVC4::parser::ParserBuilder. ** diff --git a/test/unit/prop/cnf_stream_white.h b/test/unit/prop/cnf_stream_white.h index f76a1e4d3..bf28e5996 100644 --- a/test/unit/prop/cnf_stream_white.h +++ b/test/unit/prop/cnf_stream_white.h @@ -1,13 +1,13 @@ /********************* */ /*! \file cnf_stream_white.h ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: Dejan Jovanovic, Christopher L. Conway - ** Minor contributors (to current version): Liana Hadarean + ** Top contributors (to current version): + ** Morgan Deters, Christopher L. Conway, Dejan Jovanovic ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim ** ** \brief White box testing of CVC4::prop::CnfStream. ** diff --git a/test/unit/theory/logic_info_white.h b/test/unit/theory/logic_info_white.h index 1d363ec9c..6332563ed 100644 --- a/test/unit/theory/logic_info_white.h +++ b/test/unit/theory/logic_info_white.h @@ -1,13 +1,13 @@ /********************* */ /*! \file logic_info_white.h ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: none - ** Minor contributors (to current version): Kshitij Bansal, Tianyi Liang + ** Top contributors (to current version): + ** Morgan Deters, Tim King, Martin Brain ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim ** ** \brief Unit testing for CVC4::LogicInfo class ** diff --git a/test/unit/theory/theory_arith_white.h b/test/unit/theory/theory_arith_white.h index 49231071b..fae2f6e76 100644 --- a/test/unit/theory/theory_arith_white.h +++ b/test/unit/theory/theory_arith_white.h @@ -1,13 +1,13 @@ /********************* */ /*! \file theory_arith_white.h ** \verbatim - ** Original author: Tim King - ** Major contributors: Morgan Deters - ** Minor contributors (to current version): Kshitij Bansal, Dejan Jovanovic + ** Top contributors (to current version): + ** Tim King, Morgan Deters, Dejan Jovanovic ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim ** ** \brief [[ Add one-line brief description here ]] ** diff --git a/test/unit/theory/theory_black.h b/test/unit/theory/theory_black.h index fe8bebdbf..759f56380 100644 --- a/test/unit/theory/theory_black.h +++ b/test/unit/theory/theory_black.h @@ -1,13 +1,13 @@ /********************* */ /*! \file theory_black.h ** \verbatim - ** Original author: Tim King - ** Major contributors: Clark Barrett - ** Minor contributors (to current version): Liana Hadarean + ** Top contributors (to current version): + ** Clark Barrett, Tim King, Liana Hadarean ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim ** ** \brief Black box testing of CVC4::theory ** diff --git a/test/unit/theory/theory_bv_white.h b/test/unit/theory/theory_bv_white.h index 8fddf7394..49cba9bf8 100644 --- a/test/unit/theory/theory_bv_white.h +++ b/test/unit/theory/theory_bv_white.h @@ -1,13 +1,13 @@ /********************* */ /*! \file theory_bv_white.h ** \verbatim - ** Original author: Liana Hadarean - ** Major contributors: none - ** Minor contributors (to current version): Morgan Deters + ** Top contributors (to current version): + ** Liana Hadarean, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim ** ** \brief [[ Add one-line brief description here ]] ** diff --git a/test/unit/theory/theory_engine_white.h b/test/unit/theory/theory_engine_white.h index e72b2cf4d..1c19a847c 100644 --- a/test/unit/theory/theory_engine_white.h +++ b/test/unit/theory/theory_engine_white.h @@ -1,13 +1,13 @@ /********************* */ /*! \file theory_engine_white.h ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: Dejan Jovanovic - ** Minor contributors (to current version): Andrew Reynolds, Christopher L. Conway, Tim King + ** Top contributors (to current version): + ** Morgan Deters, Dejan Jovanovic, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim ** ** \brief White box testing of CVC4::theory::Theory. ** diff --git a/test/unit/theory/theory_white.h b/test/unit/theory/theory_white.h index 9a0cbeea4..05691373b 100644 --- a/test/unit/theory/theory_white.h +++ b/test/unit/theory/theory_white.h @@ -1,13 +1,13 @@ /********************* */ /*! \file theory_white.h ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: Tim King - ** Minor contributors (to current version): Dejan Jovanovic, Clark Barrett + ** Top contributors (to current version): + ** Tim King, Morgan Deters, Clark Barrett ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim ** ** \brief Black box testing of CVC4::theory::Theory. ** diff --git a/test/unit/theory/type_enumerator_white.h b/test/unit/theory/type_enumerator_white.h index 993021c5a..b33f7bd73 100644 --- a/test/unit/theory/type_enumerator_white.h +++ b/test/unit/theory/type_enumerator_white.h @@ -1,13 +1,13 @@ /********************* */ /*! \file type_enumerator_white.h ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: none - ** Minor contributors (to current version): none + ** Top contributors (to current version): + ** Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim ** ** \brief White box testing of CVC4::theory::TypeEnumerator ** diff --git a/test/unit/util/array_store_all_black.h b/test/unit/util/array_store_all_black.h index 6a75bc7fa..6465a6301 100644 --- a/test/unit/util/array_store_all_black.h +++ b/test/unit/util/array_store_all_black.h @@ -1,13 +1,13 @@ /********************* */ /*! \file array_store_all_black.h ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: none - ** Minor contributors (to current version): none + ** Top contributors (to current version): + ** Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim ** ** \brief Black box testing of CVC4::ArrayStoreAll ** diff --git a/test/unit/util/assert_white.h b/test/unit/util/assert_white.h index bbc4d02b3..efc069246 100644 --- a/test/unit/util/assert_white.h +++ b/test/unit/util/assert_white.h @@ -1,13 +1,13 @@ /********************* */ /*! \file assert_white.h ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: none - ** Minor contributors (to current version): none + ** Top contributors (to current version): + ** Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim ** ** \brief White box testing of CVC4::Configuration. ** diff --git a/test/unit/util/binary_heap_black.h b/test/unit/util/binary_heap_black.h index 41e4d0e75..54241ee8e 100644 --- a/test/unit/util/binary_heap_black.h +++ b/test/unit/util/binary_heap_black.h @@ -1,13 +1,13 @@ /********************* */ /*! \file binary_heap_black.h ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: none - ** Minor contributors (to current version): none + ** Top contributors (to current version): + ** Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim ** ** \brief Black box testing of CVC4::BinaryHeap ** diff --git a/test/unit/util/bitvector_black.h b/test/unit/util/bitvector_black.h index b93bfafc3..0b58b1b63 100644 --- a/test/unit/util/bitvector_black.h +++ b/test/unit/util/bitvector_black.h @@ -1,13 +1,13 @@ /********************* */ /*! \file bitvector_black.h ** \verbatim - ** Original author: Christopher L. Conway - ** Major contributors: Morgan Deters - ** Minor contributors (to current version): none + ** Top contributors (to current version): + ** Christopher L. Conway, Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim ** ** \brief Black box testing of CVC4::BitVector ** diff --git a/test/unit/util/boolean_simplification_black.h b/test/unit/util/boolean_simplification_black.h index 4c0eb81cc..cb5e20db9 100644 --- a/test/unit/util/boolean_simplification_black.h +++ b/test/unit/util/boolean_simplification_black.h @@ -1,13 +1,13 @@ /********************* */ /*! \file boolean_simplification_black.h ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: none - ** Minor contributors (to current version): none + ** Top contributors (to current version): + ** Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim ** ** \brief Black box testing of CVC4::BooleanSimplification ** diff --git a/test/unit/util/cardinality_public.h b/test/unit/util/cardinality_public.h index 2fcee66b6..7d7c67506 100644 --- a/test/unit/util/cardinality_public.h +++ b/test/unit/util/cardinality_public.h @@ -1,13 +1,13 @@ /********************* */ /*! \file cardinality_public.h ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: none - ** Minor contributors (to current version): none + ** Top contributors (to current version): + ** Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim ** ** \brief Public-box testing of CVC4::Cardinality ** diff --git a/test/unit/util/configuration_black.h b/test/unit/util/configuration_black.h index f07763595..72a887f65 100644 --- a/test/unit/util/configuration_black.h +++ b/test/unit/util/configuration_black.h @@ -1,13 +1,13 @@ /********************* */ /*! \file configuration_black.h ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: none - ** Minor contributors (to current version): none + ** Top contributors (to current version): + ** Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim ** ** \brief Black box testing of CVC4::Configuration. ** diff --git a/test/unit/util/datatype_black.h b/test/unit/util/datatype_black.h index 91a53ddc3..d812747f5 100644 --- a/test/unit/util/datatype_black.h +++ b/test/unit/util/datatype_black.h @@ -1,13 +1,13 @@ /********************* */ /*! \file datatype_black.h ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: none - ** Minor contributors (to current version): Andrew Reynolds + ** Top contributors (to current version): + ** Morgan Deters, Tim King, Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim ** ** \brief Black box testing of CVC4::Datatype ** diff --git a/test/unit/util/exception_black.h b/test/unit/util/exception_black.h index c2c7f83c0..71e99b6e4 100644 --- a/test/unit/util/exception_black.h +++ b/test/unit/util/exception_black.h @@ -1,13 +1,13 @@ /********************* */ /*! \file exception_black.h ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: none - ** Minor contributors (to current version): none + ** Top contributors (to current version): + ** Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim ** ** \brief Black box testing of CVC4::Exception. ** diff --git a/test/unit/util/integer_black.h b/test/unit/util/integer_black.h index 510afe7b7..563c73b66 100644 --- a/test/unit/util/integer_black.h +++ b/test/unit/util/integer_black.h @@ -1,13 +1,13 @@ /********************* */ /*! \file integer_black.h ** \verbatim - ** Original author: Tim King - ** Major contributors: Morgan Deters - ** Minor contributors (to current version): Christopher L. Conway + ** Top contributors (to current version): + ** Tim King, Morgan Deters, Christopher L. Conway ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim ** ** \brief Black box testing of CVC4::Integer. ** diff --git a/test/unit/util/integer_white.h b/test/unit/util/integer_white.h index 12eabfbb2..b4e4129a2 100644 --- a/test/unit/util/integer_white.h +++ b/test/unit/util/integer_white.h @@ -1,13 +1,13 @@ /********************* */ /*! \file integer_white.h ** \verbatim - ** Original author: Tim King - ** Major contributors: Morgan Deters - ** Minor contributors (to current version): none + ** Top contributors (to current version): + ** Tim King, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim ** ** \brief White box testing of CVC4::Integer. ** diff --git a/test/unit/util/listener_black.h b/test/unit/util/listener_black.h index 682a7c67b..5319eacd1 100644 --- a/test/unit/util/listener_black.h +++ b/test/unit/util/listener_black.h @@ -1,13 +1,13 @@ /********************* */ -/*! \file output_black.h +/*! \file listener_black.h ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: none - ** Minor contributors (to current version): none + ** Top contributors (to current version): + ** Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim ** ** \brief Black box testing of CVC4 output classes. ** @@ -137,7 +137,7 @@ public: } TS_ASSERT(not collection.empty()); - for(int i=0; i < listeners.size(); ++i){ + for(unsigned i=0; i < listeners.size(); ++i){ ListenerCollection::Registration* at_i = listeners[i]; delete at_i; } diff --git a/test/unit/util/output_black.h b/test/unit/util/output_black.h index 369f5b673..33a0934de 100644 --- a/test/unit/util/output_black.h +++ b/test/unit/util/output_black.h @@ -1,13 +1,13 @@ /********************* */ /*! \file output_black.h ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: none - ** Minor contributors (to current version): none + ** Top contributors (to current version): + ** Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim ** ** \brief Black box testing of CVC4 output classes. ** diff --git a/test/unit/util/rational_black.h b/test/unit/util/rational_black.h index d25c9473c..aa5e8656e 100644 --- a/test/unit/util/rational_black.h +++ b/test/unit/util/rational_black.h @@ -1,13 +1,13 @@ /********************* */ /*! \file rational_black.h ** \verbatim - ** Original author: Christopher L. Conway - ** Major contributors: Morgan Deters - ** Minor contributors (to current version): none + ** Top contributors (to current version): + ** Christopher L. Conway, Tim King, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim ** ** \brief Black box testing of CVC4::Rational. ** diff --git a/test/unit/util/rational_white.h b/test/unit/util/rational_white.h index dfd0fa43b..690319b97 100644 --- a/test/unit/util/rational_white.h +++ b/test/unit/util/rational_white.h @@ -1,13 +1,13 @@ /********************* */ /*! \file rational_white.h ** \verbatim - ** Original author: Tim King - ** Major contributors: none - ** Minor contributors (to current version): Morgan Deters + ** Top contributors (to current version): + ** Tim King, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim ** ** \brief White box testing of CVC4::Rational. ** diff --git a/test/unit/util/stats_black.h b/test/unit/util/stats_black.h index dd67429cf..c5b0d46bb 100644 --- a/test/unit/util/stats_black.h +++ b/test/unit/util/stats_black.h @@ -1,13 +1,13 @@ /********************* */ /*! \file stats_black.h ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: none - ** Minor contributors (to current version): Kshitij Bansal + ** Top contributors (to current version): + ** Morgan Deters, Tim King, Kshitij Bansal ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim ** ** \brief Black box testing of CVC4::Stat and associated classes ** diff --git a/test/unit/util/subrange_bound_white.h b/test/unit/util/subrange_bound_white.h index 3b785ae0d..05353aea4 100644 --- a/test/unit/util/subrange_bound_white.h +++ b/test/unit/util/subrange_bound_white.h @@ -1,13 +1,13 @@ /********************* */ /*! \file subrange_bound_white.h ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: none - ** Minor contributors (to current version): none + ** Top contributors (to current version): + ** Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim ** ** \brief White-box testing of CVC4::SubrangeBound ** |