Add some tests to ModelTest for trivial cases
@@ -76,6 +76,33 @@ public class ModelTest extends SolverBasedTest0 {
return solver;
}
+ @Test
+ public void testEmpty() throws SolverException, InterruptedException {
+ try (ProverEnvironment prover = context.newProverEnvironment(ProverOptions.GENERATE_MODELS)) {
+ assertThat(prover).isSatisfiable();
+
+ try (Model m = prover.getModel()) {
+ assertThat(m).isEmpty();
+ }
+
+ assertThat(prover.getModelAssignments()).isEmpty();
+ }
+ }
+
+ @Test
+ public void testOnlyTrue() throws SolverException, InterruptedException {
+ try (ProverEnvironment prover = context.newProverEnvironment(ProverOptions.GENERATE_MODELS)) {
+ prover.push(bmgr.makeTrue());
+ assertThat(prover).isSatisfiable();
+
+ try (Model m = prover.getModel()) {
+ assertThat(m).isEmpty();
+ }
+
+ assertThat(prover.getModelAssignments()).isEmpty();
+ }
+ }
+
@Test
public void testGetSmallIntegers() throws SolverException, InterruptedException {
testModelGetters(
