First (sbt) test to make it into master.

.gitignore

+# Vim
+*.swp
+
+# sbt
 target
 /project/build
 /leon

build.sbt

@@ -12,5 +12,10 @@ scalacOptions += "-unchecked"
 
 libraryDependencies += "org.scala-lang" % "scala-compiler" % "2.9.1-1"
 
+libraryDependencies += "org.scalatest" %% "scalatest" % "1.8" % "test"
+
 unmanagedBase <<= baseDirectory { base => base / "unmanaged" }
 
+fork in run := true
+
+fork in test := true

src/main/scala/leon/Reporter.scala

@@ -57,6 +57,11 @@ class DefaultReporter extends Reporter {
 }
 
 class QuietReporter extends DefaultReporter {
-  override def warning(msg: Any) = {}
-  override def info(msg: Any) = {}
+  override def warning(msg : Any) = {}
+  override def info(msg : Any) = {}
+}
+
+class SilentReporter extends QuietReporter {
+  override def error(msg : Any) = {}
+  override def fatalError(msg : Any) = throw new Exception("Fatal error: " + msg.toString)
 }

src/main/scala/leon/solvers/z3/UninterpretedZ3Solver.scala

@@ -52,20 +52,25 @@ class UninterpretedZ3Solver(reporter : Reporter) extends Solver(reporter) with A
 
   // Where the solving occurs
   override def solveOrGetCounterexample(expression : Expr) : (Option[Boolean],Map[Identifier,Expr]) = {
+    restartZ3
+
     val emptyModel    = Map.empty[Identifier,Expr]
     val unknownResult = (None, emptyModel)
     val validResult   = (Some(true), emptyModel)
 
-    containedInvocations = false
     val result = toZ3Formula(expression).map { asZ3 => 
       z3.assertCnstr(z3.mkNot(asZ3))
       z3.checkAndGetModel() match {
         case (Some(false), _) => validResult
-        case (Some(true), model) if !containedInvocations => {
-          val variables = variablesOf(expression)
-          val r = (Some(false), modelToMap(model, variables))
-          model.delete
-          r
+        case (Some(true), model) => {
+          if(containsFunctionCalls(expression)) {
+            unknownResult
+          } else { 
+            val variables = variablesOf(expression)
+            val r = (Some(false), modelToMap(model, variables))
+            model.delete
+            r
+          }
         }
         case _ => unknownResult
       }
@@ -73,14 +78,4 @@ class UninterpretedZ3Solver(reporter : Reporter) extends Solver(reporter) with A
 
     result
   }
-
-  private var containedInvocations : Boolean = _
-
-  override def toZ3Formula(expr : Expr, m : Map[Identifier,Z3AST] = Map.empty) : Option[Z3AST] = {
-    expr match {
-      case FunctionInvocation(_, _) => containedInvocations = true
-      case _ => ;
-    }
-    super.toZ3Formula(expr,m)
-  }
 }

src/test/scala/leon/test/solvers/z3/UninterpretedZ3SolverTests.scala

+package leon.test.solvers.z3
+
+import leon.purescala.Common._
+import leon.purescala.Definitions._
+import leon.purescala.Trees._
+import leon.purescala.TreeOps._
+import leon.purescala.TypeTrees._
+
+import leon.SilentReporter
+
+import leon.Extensions.Solver
+import leon.solvers.z3.UninterpretedZ3Solver
+
+import org.scalatest.FunSuite
+
+class UninterpretedZ3SolverTests extends FunSuite {
+  private var testCounter : Int = 0
+  private def solverCheck(solver : Solver, expr : Expr, expected : Option[Boolean], msg : String) = {
+    testCounter += 1
+
+    test("Solver test #" + testCounter) {
+      assert(solver.solve(expr) === expected, msg)
+    }
+  }
+
+  private def assertValid(solver : Solver, expr : Expr) = solverCheck(
+    solver, expr, Some(true),
+    "Solver should prove the formula " + expr + " valid."
+  )
+
+  private def assertInvalid(solver : Solver, expr : Expr) = solverCheck(
+    solver, expr, Some(false),
+    "Solver should prove the formula " + expr + " invalid."
+  )
+
+  private def assertUnknown(solver : Solver, expr : Expr) = solverCheck(
+    solver, expr, None,
+    "Solver should not be able to decide the formula " + expr + "."
+  )
+
+  private val silentReporter = new SilentReporter
+
+  // def f(fx : Int) : Int = fx + 1
+  private val fx   : Identifier = FreshIdentifier("x").setType(Int32Type)
+  private val fDef : FunDef = new FunDef(FreshIdentifier("f"), Int32Type, VarDecl(fx, Int32Type) :: Nil)
+  fDef.body = Some(Plus(Variable(fx), IntLiteral(1)))
+
+  private val minimalProgram = Program(
+    FreshIdentifier("Minimal"), 
+    ObjectDef(FreshIdentifier("Minimal"), Seq(
+      fDef
+    ), Seq.empty)
+  )
+
+  private val x : Expr = Variable(FreshIdentifier("x").setType(Int32Type))
+  private val y : Expr = Variable(FreshIdentifier("y").setType(Int32Type))
+  private def f(e : Expr) : Expr = FunctionInvocation(fDef, e :: Nil)
+
+  private val solver = new UninterpretedZ3Solver(silentReporter)
+  solver.setProgram(minimalProgram)
+
+  private val tautology1 : Expr = BooleanLiteral(true)
+  assertValid(solver, tautology1)
+
+  private val tautology2 : Expr = Equals(Plus(x, x), Times(IntLiteral(2), x))
+  assertValid(solver, tautology2)
+
+  // This one contains a function invocation but is valid regardless of its
+  // interpretation, so should be proved anyway.
+  private val tautology3 : Expr = Implies(
+    Not(Equals(f(x), f(y))),
+    Not(Equals(x, y))
+  )
+  assertValid(solver, tautology3)
+
+  private val wrong1 : Expr = BooleanLiteral(false)
+  assertInvalid(solver, wrong1)
+
+  private val wrong2 : Expr = Equals(Plus(x, x), Times(IntLiteral(3), x))
+  assertInvalid(solver, wrong2)
+
+  // This is true, but that solver shouldn't know it.
+  private val unknown1 : Expr = Equals(f(x), Plus(x, IntLiteral(1)))
+  assertUnknown(solver, unknown1)
+}