Try Z3's simple solver before the default one

liquidjava-verifier/src/main/java/liquidjava/smt/SMTEvaluator.java

@@ -40,8 +40,12 @@ public SMTResult verifySubtype(Predicate subRef, Predicate supRef, Context conte
             try (TranslatorToZ3 tz3 = new TranslatorToZ3(context)) {
                 ExpressionToZ3Visitor visitor = new ExpressionToZ3Visitor(tz3);
                 Expr<?> e = exp.accept(visitor);
-                Solver solver = tz3.makeSolverForExpression(e);
+                Solver solver = tz3.makeSimpleSolverForExpression(e);
                 Status result = solver.check();
+                if (result.equals(Status.UNKNOWN)) {
+                    solver = tz3.makeSolverForExpression(e);
+                    result = solver.check();
+                }
 
                 // subRef is not a subtype of supRef
                 if (result.equals(Status.SATISFIABLE)) {
@@ -78,8 +82,10 @@ public boolean isUnsatisfiable(Predicate predicate, Context context) throws Exce
             try (TranslatorToZ3 tz3 = new TranslatorToZ3(context)) {
                 ExpressionToZ3Visitor visitor = new ExpressionToZ3Visitor(tz3);
                 Expr<?> e = exp.accept(visitor);
-                Solver solver = tz3.makeSolverForExpression(e);
-                return solver.check().equals(Status.UNSATISFIABLE);
+                Status result = tz3.makeSimpleSolverForExpression(e).check();
+                if (result.equals(Status.UNKNOWN))
+                    result = tz3.makeSolverForExpression(e).check();
+                return result.equals(Status.UNSATISFIABLE);
             }
         } catch (Z3Exception e) {
             throw new Z3Exception(e.getLocalizedMessage());

liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java

@@ -8,6 +8,7 @@
 import com.microsoft.z3.FuncDecl;
 import com.microsoft.z3.IntExpr;
 import com.microsoft.z3.IntNum;
+import com.microsoft.z3.Params;
 import com.microsoft.z3.RealExpr;
 import com.microsoft.z3.Solver;
 import com.microsoft.z3.Sort;
@@ -36,6 +37,12 @@
 
 public class TranslatorToZ3 implements AutoCloseable {
 
+    /**
+     * Deterministic work budget of the simple solver. Queries it decides use at most about a thousand units; ones it
+     * cannot decide can take millions, and minutes, before it gives up
+     */
+    private static final int SIMPLE_SOLVER_RLIMIT = 100_000;
+
     private final com.microsoft.z3.Context z3 = new com.microsoft.z3.Context();
     private final Map<String, Expr<?>> varTranslation = new HashMap<>();
     private final Map<String, List<Expr<?>>> varSuperTypes = new HashMap<>();
@@ -66,9 +73,26 @@ public TranslatorToZ3(liquidjava.processor.context.Context context) {
         TranslatorContextToZ3.addGhostStates(z3, context.getGhostStates(), funcTranslation);
     }
 
-    @SuppressWarnings("unchecked")
     public Solver makeSolverForExpression(Expr<?> e) {
-        Solver solver = z3.mkSolver();
+        return addToSolver(z3.mkSolver(), e);
+    }
+
+    /**
+     * A solver for {@code e} without the preprocessing tactics of the default solver, which take most of the time of
+     * the small queries the verifier asks. It decides fewer queries and can get stuck on the ones it cannot decide, so
+     * it gives up after {@link #SIMPLE_SOLVER_RLIMIT} and an unknown result should be retried with
+     * {@link #makeSolverForExpression}
+     */
+    public Solver makeSimpleSolverForExpression(Expr<?> e) {
+        Solver solver = z3.mkSimpleSolver();
+        Params params = z3.mkParams();
+        params.add("rlimit", SIMPLE_SOLVER_RLIMIT);
+        solver.setParameters(params);
+        return addToSolver(solver, e);
+    }
+
+    @SuppressWarnings("unchecked")
+    private Solver addToSolver(Solver solver, Expr<?> e) {
         for (BoolExpr axiom : staticConstantAxioms)
             solver.add(axiom);
         for (BoolExpr axiom : referenceIdentityAxioms)