From 4eabdc60fd740600d6bf5a85c868e6036a50f863 Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Fri, 29 May 2015 14:53:09 +0200
Subject: [PATCH] Translate if-then-else back to leon
---
src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala | 7 +++++++
1 file changed, 7 insertions(+)
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
index 12a908276..c0dbf1e9a 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
@@ -729,6 +729,13 @@ abstract class SMTLIBSolver(val context: LeonContext,
unsupported("Unknown symbol: "+s)
}
+ case (FunctionApplication(SimpleSymbol(SSymbol("ite")), Seq(cond, thenn, elze)), t) =>
+ IfExpr(
+ fromSMT(cond, BooleanType),
+ fromSMT(thenn, t),
+ fromSMT(elze, t)
+ )
+
case (FunctionApplication(SimpleSymbol(s), args), tpe) if constructors.containsB(s) =>
constructors.toA(s) match {
case cct: CaseClassType =>
--
GitLab