Fix some bugs in new z3 solver

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

@@ -3,9 +3,10 @@ package leon.solvers.smtlib
 import leon.purescala.DefOps._
 import leon.purescala.Definitions.TypedFunDef
 import leon.purescala.ExprOps._
-import leon.purescala.Expressions.{Equals, FunctionInvocation}
+import leon.purescala.Expressions._
+import leon.purescala.Constructors._
 import smtlib.parser.Commands.{DeclareFun, Assert}
-import smtlib.parser.Terms.{Term, SortedVar, SSymbol, ForAll}
+import smtlib.parser.Terms.{ForAll => SMTForall, SSymbol}
 
 /**
  * This solver models function definitions as universally quantified formulas.
@@ -20,57 +21,56 @@ trait SMTLIBZ3QuantifiedTarget extends SMTLIBZ3Target {
   override def targetName = "z3-quantified"
 
   override def declareFunction(tfd: TypedFunDef): SSymbol = {
-    if (tfd.params.isEmpty) {
-      super[SMTLIBZ3Target].declareFunction(tfd)
-    } else {
-      val (funs, exploredAll) = typedTransitiveCallees(Set(tfd), Some(typedFunDefExplorationLimit))
-      if (!exploredAll) {
-        reporter.warning(
-          s"Did not manage to explore the space of typed functions called from ${tfd.id}. The solver may fail"
-        )
-      }
 
-      val smtFunDecls = funs.toSeq.collect {
-        case tfd if !functions.containsA(tfd) && tfd.params.nonEmpty =>
-          val id = if (tfd.tps.isEmpty) {
-            tfd.id
-          } else {
-            tfd.id.freshen
-          }
-          val sym = id2sym(id)
-          functions +=(tfd, sym)
-          sendCommand(DeclareFun(
-            sym,
-            tfd.params map { p => declareSort(p.getType) },
-            declareSort(tfd.returnType)
-          ))
-          sym
-      }
-      smtFunDecls foreach { sym =>
-        val tfd = functions.toA(sym)
-        val sortedVars = tfd.params.map { p =>
-          SortedVar(id2sym(p.id), declareSort(p.getType))
-        }
-        val term =
-          if (sortedVars.isEmpty) {
-            toSMT(Equals(FunctionInvocation(tfd, Seq()), tfd.body.get))(Map())
-          } else {
-            ForAll(
-              sortedVars.head,
-              sortedVars.tail,
-              toSMT(Equals(
-                FunctionInvocation(tfd, tfd.params.map {_.toVariable}),
-                matchToIfThenElse(tfd.body.get)
-              ))(
-                tfd.params.map { p => (p.id, id2sym(p.id): Term) }.toMap
-              )
-            )
+    val (funs, exploredAll) = typedTransitiveCallees(Set(tfd), Some(typedFunDefExplorationLimit))
+    if (!exploredAll) {
+      reporter.warning(
+        s"Did not manage to explore the space of typed functions called from ${tfd.id}. The solver may fail"
+      )
+    }
+
+    val smtFunDecls = funs.toSeq.collect {
+      case tfd if !functions.containsA(tfd) =>
+        val id = if (tfd.tps.isEmpty) {
+          tfd.id
+        } else {
+          tfd.id.freshen
         }
-        sendCommand(Assert(term))
-      }
+        val sym = id2sym(id)
+        functions +=(tfd, sym)
+        sendCommand(DeclareFun(
+          sym,
+          tfd.params map { p => declareSort(p.getType) },
+          declareSort(tfd.returnType)
+        ))
+        sym
+    }
+    smtFunDecls foreach { sym =>
+      val tfd = functions.toA(sym)
+      val term = quantifiedTerm(
+        SMTForall,
+        tfd.params map { _.id },
+        matchToIfThenElse(Equals(
+          FunctionInvocation(tfd, tfd.params.map {_.toVariable}),
+          matchToIfThenElse(tfd.body.get)
+        ))
+      )
+      sendCommand(Assert(term))
 
-      functions.toB(tfd)
+      tfd.postcondition foreach { post =>
+        val axiom = matchToIfThenElse(implies(
+          tfd.precondition getOrElse BooleanLiteral(true),
+          application(
+            post,
+            Seq(FunctionInvocation(tfd, tfd.params map { _.toVariable }))
+          )
+        ))
+        sendCommand(Assert(quantifiedTerm(SMTForall, axiom)))
+      }
     }
+
+    functions.toB(tfd)
   }
 
+
 }