Improve test for models of UFs
This triggers a bug in SmtInterpolModel
@@ -155,21 +155,10 @@ public class ModelTest extends SolverBasedTest0 {
IntegerFormula app1 = fmgr.callUF(declaration, arg1);
IntegerFormula app2 = fmgr.callUF(declaration, arg2);
- try (ProverEnvironment prover = context.newProverEnvironment(ProverOptions.GENERATE_MODELS)) {
- prover.push(imgr.equal(app1, imgr.makeNumber(1)));
- prover.push(imgr.equal(app2, imgr.makeNumber(2)));
- prover.push(imgr.equal(arg1, imgr.makeNumber(3)));
- prover.push(imgr.equal(arg2, imgr.makeNumber(4)));
-
- assertThat(prover).isSatisfiable();
-
- try (Model m = prover.getModel()) {
- assertThat(m.evaluate(app1)).isEqualTo(BigInteger.ONE);
- assertThat(m.evaluate(app2)).isEqualTo(BigInteger.valueOf(2));
- assertThat(m)
- .containsExactly(
+ ImmutableList<ValueAssignment> expectedModel =
+ ImmutableList.of(
new ValueAssignment(arg1, "arg1", BigInteger.valueOf(3), ImmutableList.of()),
- new ValueAssignment(arg1, "arg2", BigInteger.valueOf(4), ImmutableList.of()),
+ new ValueAssignment(arg2, "arg2", BigInteger.valueOf(4), ImmutableList.of()),
new ValueAssignment(
fmgr.callUF(declaration, imgr.makeNumber(3)),
"UF",
@@ -180,7 +169,21 @@ public class ModelTest extends SolverBasedTest0 {
"UF",
BigInteger.valueOf(2),
ImmutableList.of(BigInteger.valueOf(4))));
+
+ try (ProverEnvironment prover = context.newProverEnvironment(ProverOptions.GENERATE_MODELS)) {
+ prover.push(
+ bmgr.and(imgr.equal(app1, imgr.makeNumber(1)), imgr.equal(app2, imgr.makeNumber(2))));
+ prover.push(imgr.equal(arg1, imgr.makeNumber(3)));
+ prover.push(imgr.equal(arg2, imgr.makeNumber(4)));
+
+ assertThat(prover).isSatisfiable();
+
+ try (Model m = prover.getModel()) {
+ assertThat(m.evaluate(app1)).isEqualTo(BigInteger.ONE);
+ assertThat(m.evaluate(app2)).isEqualTo(BigInteger.valueOf(2));
+ assertThat(m).containsExactlyElementsIn(expectedModel);
}
+ assertThat(prover.getModelAssignments()).containsExactlyElementsIn(expectedModel);
}
}
