@@ -0,0 +1,816 @@
+package de.bmoth.issues;%0A%0Aimport com.microsoft.z3.BoolExpr;%0Aimport com.microsoft.z3.Model;%0Aimport de.bmoth.TestUsingZ3;%0Aimport de.bmoth.backend.z3.FormulaToZ3Translator;%0Aimport de.bmoth.backend.z3.SolutionFinder;%0Aimport org.junit.Ignore;%0Aimport org.junit.Test;%0A%0Aimport java.io.IOException;%0Aimport java.util.Set;%0A%0Aimport static org.junit.Assert.assertEquals;%0A%0Apublic class Issue73Test extends TestUsingZ3 %7B%0A    @Test%0A    @Ignore%0A    public void testSatPredicateWithoutModel() throws IOException %7B%0A        String formula = %221 %3C 2%22;%0A        BoolExpr constraint = FormulaToZ3Translator.translatePredicate(formula, z3Context);%0A%0A        SolutionFinder finder = new SolutionFinder(constraint, z3Solver, z3Context);%0A        Set%3CModel%3E solutions = finder.findSolutions(20);%0A        assertEquals(1, solutions.size());%0A    %7D%0A%7D%0A

add test showing #73