Disable interpolation for CVC5 as the Java API for it has problems
making it unuseable at the moment
@@ -64,6 +64,7 @@ public final class CVC5SolverContext extends AbstractSolverContext {
// Set Strings option to enable all String features (such as lessOrEquals)
newSolver.setOption("strings-exp", "true");
newSolver.setOption("produce-unsat-cores", "true");
+ newSolver.setOption("produce-interpols", "all");
// Neither simplification, arith-rewrite-equalities, pb-rewrites provide rewrites of trivial
// formulas only
// Note: with solver.getOptionNames() you can get all options
@@ -143,13 +144,14 @@ public final class CVC5SolverContext extends AbstractSolverContext {
@Override
protected InterpolatingProverEnvironment<?> newProverEnvironmentWithInterpolation0(
Set<ProverOptions> pSet) {
- // FIXME
- return null;
+ // CVC5 DOES support interpolation, but the Java API needs fixes and will only be available in
+ // the next release
+ throw new UnsupportedOperationException("CVC5 does not support interpolation");
}
@Override
protected OptimizationProverEnvironment newOptimizationProverEnvironment0(
Set<ProverOptions> pSet) {
- throw new UnsupportedOperationException("CVC4 does not support optimization");
+ throw new UnsupportedOperationException("CVC5 does not support optimization");
}
}
