Last-minute matchToIfThenElse, when not done by templates.

src/main/scala/leon/solvers/smtlib/SMTLIBCVC4QuantifiedTarget.scala

@@ -6,9 +6,8 @@ package solvers.smtlib
 import purescala.Common.FreshIdentifier
 import purescala.Expressions.{FunctionInvocation, BooleanLiteral, Expr, Implies}
 import purescala.Definitions.TypedFunDef
-import purescala.Constructors.application
+import purescala.Constructors.{application, implies}
 import purescala.DefOps.typedTransitiveCallees
-import leon.purescala.ExprOps.matchToIfThenElse
 import smtlib.parser.Commands._
 import smtlib.parser.Terms._
 import smtlib.theories.Core.Equals
@@ -43,13 +42,13 @@ trait SMTLIBCVC4QuantifiedTarget extends SMTLIBCVC4Target {
 
       functions +=(tfd, id2sym(id))
 
-      val bodyAssert = Assert(Equals(id2sym(id): Term, toSMT(matchToIfThenElse(tfd.body.get))(Map())))
+      val bodyAssert = Assert(Equals(id2sym(id): Term, toSMT(tfd.body.get)(Map())))
 
       val specAssert = tfd.postcondition map { post =>
-        val term = matchToIfThenElse(Implies(
+        val term = implies(
           tfd.precondition getOrElse BooleanLiteral(true),
           application(post, Seq(FunctionInvocation(tfd, Seq())))
-        ))
+        )
         Assert(toSMT(term)(Map()))
       }
 
@@ -75,7 +74,7 @@ trait SMTLIBCVC4QuantifiedTarget extends SMTLIBCVC4Target {
 
     val smtBodies = smtFunDecls map { case FunDec(sym, _, _) =>
       val tfd = functions.toA(sym)
-      toSMT(matchToIfThenElse(tfd.body.get))(tfd.params.map { p =>
+      toSMT(tfd.body.get)(tfd.params.map { p =>
         (p.id, id2sym(p.id): Term)
       }.toMap)
     }
@@ -87,10 +86,10 @@ trait SMTLIBCVC4QuantifiedTarget extends SMTLIBCVC4Target {
         tfd <- seen
         post <- tfd.postcondition
       } {
-        val term = matchToIfThenElse(Implies(
+        val term = implies(
           tfd.precondition getOrElse BooleanLiteral(true),
           application(post, Seq(FunctionInvocation(tfd, tfd.params map { _.toVariable})))
-        ))
+        )
         sendCommand(Assert(quantifiedTerm(ForAll, term)))
       }
     }

src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala

@@ -505,6 +505,13 @@ trait SMTLIBTarget {
           someTester(vt),
           Seq(ArraysEx.Select(toSMT(m), toSMT(k)))
         )
+
+      case p : Passes =>
+        toSMT(matchToIfThenElse(p.asConstraint))
+
+      case m : MatchExpr =>
+        toSMT(matchToIfThenElse(m))
+
       /**
        * ===== Everything else =====
        */
@@ -575,7 +582,6 @@ trait SMTLIBTarget {
           case _ => reporter.fatalError("Unhandled nary "+e)
         }
 
-
       case o => unsupported("Tree: " + o)
     }
   }

src/main/scala/leon/solvers/smtlib/SMTLIBZ3QuantifiedTarget.scala

@@ -50,21 +50,21 @@ trait SMTLIBZ3QuantifiedTarget extends SMTLIBZ3Target {
       val term = quantifiedTerm(
         SMTForall,
         tfd.params map { _.id },
-        matchToIfThenElse(Equals(
+        Equals(
           FunctionInvocation(tfd, tfd.params.map {_.toVariable}),
-          matchToIfThenElse(tfd.body.get)
-        ))
+          tfd.body.get
+        )
       )
       sendCommand(Assert(term))
 
       tfd.postcondition foreach { post =>
-        val axiom = matchToIfThenElse(implies(
+        val axiom = implies(
           tfd.precondition getOrElse BooleanLiteral(true),
           application(
             post,
             Seq(FunctionInvocation(tfd, tfd.params map { _.toVariable }))
           )
-        ))
+        )
         sendCommand(Assert(quantifiedTerm(SMTForall, axiom)))
       }
     }