Add a model test that checks error when requesting a model for UNSAT (do we have this already elsewhere?)

Author: BaierD

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

@@ -2431,6 +2431,32 @@ public void testDeeplyNestedFormulaBV() throws SolverException, InterruptedExcep
         var -> bvmgr.equal(var, bvmgr.makeBitvector(4, 1)));
   }
 
+  @Test
+  public void testModelAfterUnsatInt() throws SolverException, InterruptedException {
+    requireIntegers();
+    try (ProverEnvironment prover = context.newProverEnvironment(ProverOptions.GENERATE_MODELS)) {
+      HardIntegerFormulaGenerator gen = new HardIntegerFormulaGenerator(imgr, bmgr);
+      prover.push(gen.generate(8));
+
+      assertThat(prover).isUnsatisfiable();
+
+      assertThrows(IllegalStateException.class, prover::getModel);
+    }
+  }
+
+  @Test
+  public void testModelAfterUnsatBv() throws SolverException, InterruptedException {
+    requireBitvectors();
+    try (ProverEnvironment prover = context.newProverEnvironment(ProverOptions.GENERATE_MODELS)) {
+      HardBitvectorFormulaGenerator gen = new HardBitvectorFormulaGenerator(bvmgr, bmgr);
+      prover.push(gen.generate(8));
+
+      assertThat(prover).isUnsatisfiable();
+
+      assertThrows(IllegalStateException.class, prover::getModel);
+    }
+  }
+
   /**
    * Build a deep nesting that is easy to solve and can not be simplified by the solver. If any part
    * of JavaSMT or the solver tries to analyse all branches of this formula, the runtime is
@@ -2459,7 +2485,9 @@ private <T> void testDeeplyNestedFormula(
   private void evaluateInModel(BooleanFormula constraint, Formula variable, Object expectedValue)
       throws SolverException, InterruptedException {
 
-    try (ProverEnvironment prover = context.newProverEnvironment(ProverOptions.GENERATE_MODELS)) {
+    try (ProverEnvironment prover =
+        context.newProverEnvironment(
+            ProverOptions.GENERATE_MODELS, ProverOptions.GENERATE_UNSAT_CORE)) {
       prover.push(constraint);
       assertThat(prover).isSatisfiable();