#351: add tests for option combinations with unsat-core.

Author: kfriedberger

src/org/sosy_lab/java_smt/test/ProverEnvironmentTest.java

@@ -148,4 +148,41 @@ public void unsatCoreWithAssumptionsTest() throws SolverException, InterruptedEx
       assertThat(unsatCore).containsExactly(bmgr.not(selector));
     }
   }
+
+  @Test
+  public void testSatWithUnsatUnsatCoreOptions() throws InterruptedException, SolverException {
+    requireUnsatCore();
+    try (ProverEnvironment prover = context.newProverEnvironment(GENERATE_UNSAT_CORE)) {
+      checkSimpleQuery(prover);
+    }
+
+    requireUnsatCoreOverAssumptions();
+    try (ProverEnvironment prover =
+        context.newProverEnvironment(GENERATE_UNSAT_CORE_OVER_ASSUMPTIONS)) {
+      checkSimpleQuery(prover);
+    }
+
+    try (ProverEnvironment prover =
+        context.newProverEnvironment(GENERATE_UNSAT_CORE, GENERATE_UNSAT_CORE_OVER_ASSUMPTIONS)) {
+      checkSimpleQuery(prover);
+    }
+  }
+
+  private void checkSimpleQuery(ProverEnvironment pProver)
+      throws InterruptedException, SolverException {
+    BooleanFormula constraint = bmgr.implication(bmgr.makeVariable("a"), bmgr.makeVariable("b"));
+
+    {
+      pProver.push(constraint);
+      assertThat(pProver.isUnsat()).isFalse();
+      pProver.pop();
+    }
+
+    {
+      pProver.push();
+      pProver.addConstraint(constraint); // Z3 crashed here
+      assertThat(pProver.isUnsat()).isFalse();
+      pProver.pop();
+    }
+  }
 }

src/org/sosy_lab/java_smt/test/SolverBasedTest0.java

@@ -335,6 +335,13 @@ protected void requireUnsatCore() {
         .isNoneOf(Solvers.BOOLECTOR, Solvers.OPENSMT);
   }
 
+  protected void requireUnsatCoreOverAssumptions() {
+    assume()
+        .withMessage("Solver %s does not support unsat core generation", solverToUse())
+        .that(solverToUse())
+        .isNotEqualTo(Solvers.PRINCESS);
+  }
+
   protected void requireSubstitution() {
     assume()
         .withMessage("Solver %s does not support formula substitution", solverToUse())