From cc9fc875df61a6d6abeb99169131b3f5d53c52aa Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Mika=C3=ABl=20Mayer?= <mikael.mayer@epfl.ch>
Date: Wed, 20 Jan 2016 16:01:05 +0100
Subject: [PATCH] Added missing UninterpretedZ3Solver, source of many failed
tests.
---
src/main/scala/leon/solvers/SolverFactory.scala | 2 ++
src/test/scala/leon/test/LeonRegressionSuite.scala | 2 +-
2 files changed, 3 insertions(+), 1 deletion(-)
diff --git a/src/main/scala/leon/solvers/SolverFactory.scala b/src/main/scala/leon/solvers/SolverFactory.scala
index f59087bee..6b2d4272b 100644
--- a/src/main/scala/leon/solvers/SolverFactory.scala
+++ b/src/main/scala/leon/solvers/SolverFactory.scala
@@ -156,6 +156,8 @@ object SolverFactory {
SolverFactory(() => new SMTLIBCVC4Solver(ctx, program) with TimeoutSolver)
} else if(names contains "smt-z3") {
SolverFactory(() => new SMTLIBZ3Solver(ctx, program) with TimeoutSolver)
+ } else if ((names contains "fairz3") && hasNativeZ3) {
+ SolverFactory(() => new UninterpretedZ3Solver(ctx, program) with TimeoutSolver)
} else {
ctx.reporter.fatalError("No SMT solver available: native Z3 api could not load and 'cvc4' or 'z3' binaries were not found in PATH.")
}
diff --git a/src/test/scala/leon/test/LeonRegressionSuite.scala b/src/test/scala/leon/test/LeonRegressionSuite.scala
index 58fdce2c6..4181fee97 100644
--- a/src/test/scala/leon/test/LeonRegressionSuite.scala
+++ b/src/test/scala/leon/test/LeonRegressionSuite.scala
@@ -33,7 +33,7 @@ trait LeonRegressionSuite extends FunSuite with Timeouts {
body
} catch {
case fe: LeonFatalError =>
- throw new TestFailedException("Uncaught LeonFatalError", fe, 5)
+ throw new TestFailedException("Uncaught LeonFatalError" + fe.msg.map(": " + _).getOrElse(""), fe, 5)
}
}
}
--
GitLab