Skip to content
Snippets Groups Projects
Commit 4eabdc60 authored by Manos Koukoutos's avatar Manos Koukoutos
Browse files

Translate if-then-else back to leon

parent 619a6424
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
+ 7
− 0
View file @ 4eabdc60
...@@ -729,6 +729,13 @@ abstract class SMTLIBSolver(val context: LeonContext, ...@@ -729,6 +729,13 @@ abstract class SMTLIBSolver(val context: LeonContext,
unsupported("Unknown symbol: "+s) 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) => case (FunctionApplication(SimpleSymbol(s), args), tpe) if constructors.containsB(s) =>
constructors.toA(s) match { constructors.toA(s) match {
case cct: CaseClassType => case cct: CaseClassType =>
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment