diff --git a/src/main/scala/leon/solvers/SolverFactory.scala b/src/main/scala/leon/solvers/SolverFactory.scala index f59087beed61b5cf9ca9c9b1eac46ce3a7cdcbb6..6b2d4272b37b4a06ba2731c5049bcc043b87c927 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 58fdce2c6b789ddae0bbaee845f54ad6fe09de2c..4181fee97e7a4a38e3f30349458366ba62138d12 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) } } }