Skip to content
Snippets Groups Projects
Commit 42334a24 authored by Emmanouil (Manos) Koukoutos's avatar Emmanouil (Manos) Koukoutos Committed by Etienne Kneuss
Browse files

Small non-functional benchmark changes

parent 827c54c3
Branches
Tags
No related merge requests found
...@@ -145,7 +145,7 @@ object Desugar { ...@@ -145,7 +145,7 @@ object Desugar {
@induct @induct
def desugar(e : Trees.Expr) : SimpleE = { e match { def desugar(e : Trees.Expr) : SimpleE = { e match {
case Trees.Plus (lhs, rhs) => Neg(desugar(lhs)) // FIXME: Complete nonsense. Leon can't disprove it, uses example... case Trees.Plus (lhs, rhs) => Neg(desugar(lhs)) // FIXME: Complete nonsense
case Trees.Minus(lhs, rhs) => Plus(desugar(lhs), Neg(desugar(rhs))) case Trees.Minus(lhs, rhs) => Plus(desugar(lhs), Neg(desugar(rhs)))
case Trees.LessThan(lhs, rhs) => LessThan(desugar(lhs), desugar(rhs)) case Trees.LessThan(lhs, rhs) => LessThan(desugar(lhs), desugar(rhs))
case Trees.And (lhs, rhs) => Ite(desugar(lhs), desugar(rhs), Literal(0)) case Trees.And (lhs, rhs) => Ite(desugar(lhs), desugar(rhs), Literal(0))
......
...@@ -153,8 +153,9 @@ object Desugar { ...@@ -153,8 +153,9 @@ object Desugar {
case Trees.Not(e) => Ite(desugar(e), Literal(0), Literal(1)) case Trees.Not(e) => Ite(desugar(e), Literal(0), Literal(1))
case Trees.Eq(lhs, rhs) => case Trees.Eq(lhs, rhs) =>
Eq(desugar(lhs), desugar(rhs)) Eq(desugar(lhs), desugar(rhs))
// FIXME switched the branches case Trees.Ite(cond, thn, els) =>
case Trees.Ite(cond, thn, els) => Ite(desugar(cond), desugar(els), desugar(thn)) // FIXME switched the branches
Ite(desugar(cond), desugar(els), desugar(thn))
case Trees.IntLiteral(v) => Literal(v) case Trees.IntLiteral(v) => Literal(v)
case Trees.BoolLiteral(b) => Literal(b2i(b)) case Trees.BoolLiteral(b) => Literal(b2i(b))
}} ensuring { res => }} ensuring { res =>
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment