Skip to content
Snippets Groups Projects
Commit cc9fc875 authored by Mikaël Mayer's avatar Mikaël Mayer
Browse files

Added missing UninterpretedZ3Solver, source of many failed tests.

parent c2015e43
No related branches found
No related tags found
No related merge requests found
......@@ -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.")
}
......
......@@ -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)
}
}
}
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment