From 382f1a2f9652f79b44851aa4c97c5c0582e5013f Mon Sep 17 00:00:00 2001
From: Nicolas Voirol <voirol.nicolas@gmail.com>
Date: Wed, 30 Nov 2016 13:16:53 +0100
Subject: [PATCH] Extend supported fragment in AbstractPrincessSolver
---
.../inox/solvers/princess/AbstractPrincessSolver.scala | 7 +++++--
1 file changed, 5 insertions(+), 2 deletions(-)
diff --git a/src/main/scala/inox/solvers/princess/AbstractPrincessSolver.scala b/src/main/scala/inox/solvers/princess/AbstractPrincessSolver.scala
index 0ea14f242..48b4008fc 100644
--- a/src/main/scala/inox/solvers/princess/AbstractPrincessSolver.scala
+++ b/src/main/scala/inox/solvers/princess/AbstractPrincessSolver.scala
@@ -216,6 +216,9 @@ trait AbstractPrincessSolver extends AbstractSolver with ADTManagers {
case AsInstanceOf(expr, tpe) =>
parseTerm(expr)
+ case BooleanLiteral(true) => i(0)
+ case BooleanLiteral(false) => i(1)
+
// @nv: this MUST come at least after having dealt with FunctionInvocation,
// Application and ADTSelectors which can return booleans
case IsTyped(_, BooleanType) =>
@@ -252,14 +255,14 @@ trait AbstractPrincessSolver extends AbstractSolver with ADTManagers {
case Times(lhs, rhs) => {
val pLhs = parseTerm(lhs)
val pRhs = parseTerm(rhs)
- pLhs * pRhs
+ p.mult(pLhs, pRhs)
}
case UMinus(e) =>
- parseTerm(e)
case Division(lhs, rhs) =>
- p.mulTheory.eDiv(parseTerm(lhs), parseTerm(rhs))
+ p.mulTheory.tDiv(parseTerm(lhs), parseTerm(rhs))
case Remainder(lhs, rhs) =>
val q = parseTerm(Division(lhs, rhs))
--
GitLab