summaryrefslogtreecommitdiff
path: root/test/regress/regress3/quantifiers/ForElimination-scala-9.smt2
diff options
context:
space:
mode:
Diffstat (limited to 'test/regress/regress3/quantifiers/ForElimination-scala-9.smt2')
-rw-r--r--test/regress/regress3/quantifiers/ForElimination-scala-9.smt22
1 files changed, 1 insertions, 1 deletions
diff --git a/test/regress/regress3/quantifiers/ForElimination-scala-9.smt2 b/test/regress/regress3/quantifiers/ForElimination-scala-9.smt2
index 04ea50b72..91502a9e7 100644
--- a/test/regress/regress3/quantifiers/ForElimination-scala-9.smt2
+++ b/test/regress/regress3/quantifiers/ForElimination-scala-9.smt2
@@ -1,6 +1,6 @@
; COMMAND-LINE: --finite-model-find --uf-ss=no-minimal
; EXPECT: unsat
-(set-logic ALL_SUPPORTED)
+(set-logic ALL)
(declare-datatypes ((Statement!1556 0) (Expression!1578 0) (List!1617 0)) (
((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)))
((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))))
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback