[CatarinaGamboa]

Verification in the IDE is slow on specs with many state refinements. Saving any file in a study workspace (6 exercises, 15 files) re-verifies everything and took 24 s. Nearly all of it was Z3 overhead: each of the ~1,100 queries per save paid ~5 ms for the default solver's preprocessing tactics, even though the queries themselves are tiny.

This PR answers each query with Z3's simple solver first, and only falls back to the default solver (exactly as before) when the simple solver returns unknown.

The simple solver can get stuck on queries it cannot decide (one nonlinear query in liquidjava-example took 186 s before giving up, against 0.4 s for the default solver). It therefore runs with a deterministic work budget (rlimit = 100,000). Queries it decides use at most ~1,100 units (p99 in liquidjava-example; at most 837 in the study workspace). The ones it cannot decide use millions, so they go straight to the default solver. Being a resource count rather than a timeout, the budget does not depend on machine load.

Soundness: either solver's SAT/UNSAT answer is sound. A query only reaches the default solver when the simple one returns unknown. So verdicts can only stay the same, or go from unknown to decided; only the counterexample shown for a failing check could come from a different model.

Timings (warm, in the same JVM, idle machine)

	main	this PR
Study workspace (proposal-C-stars, 15 files), per save	24.0 s	8.5 s
liquidjava-example/src/main (283 files)	~142 s	84 s
Barista conformance tests (3,262 cases, total)	11,918 s*	3,048 s*

* Measured with 3 runs in parallel, so the absolute numbers are inflated; the ratio is what matters.

Same results

I compared every verdict and every diagnostic (title and position) before and after, on:

Corpus	Cases	Verdict diffs	Diagnostic diffs
testSuite (as in TestExamples)	298	0	0
liquidjava-example/src/main (whole tree)	1	0	0
Barista conformance tests (correct/ + incorrect/)	3,262	0	0
Study exercises (exercises, exercises-oss)	98	0	0

The number of SMT Unknown errors is unchanged everywhere. mvn test passes.

Where the rest of the time goes

The remaining ~8.5 s per save is mostly creating a Z3 context and declaring every context variable for each query. About 80% of it is spent on facts that depend only on the specs: the satisfiability check of each @StateRefinement while specs are registered, and building the state machine used for the state hints. They are identical on every save, so follow-up PRs will reuse them instead of recomputing them.

🤖 Generated with Claude Code

[alcides]

@claude Does LiquidFixpoint have a default tactic for z3?

[CatarinaGamboa]

No, it doesn't name a tactic. But the way it drives Z3 means it never runs the default preprocessing tactics on a normal query either, which is close to what this PR does.

What liquid-fixpoint does (Smt/Interface.hs, Smt/Theories.hs):

• It starts one z3 -smt2 -in process for the whole run (or the in-process API with z3mem) and sends it SMT-LIB text.
• The preamble only sets :auto-config false, :model true and :smt.mbqi false. There is no check-sat-using, no set-logic for Z3, and no timeout unless --smtTimeout is passed.
• Each query is wrapped in push/pop (smtBracket), followed by a plain check-sat.

Because of that push, Z3's default combined solver switches to incremental mode (combined_solver.cpp). From then on, check-sat goes straight to the SMT core and skips the tactic pipeline. If the SMT core returns unknown on a quantifier-free problem, Z3 retries with the tactic solver (combined_solver.solver2_unknown = 1 by default).

So liquid-fixpoint effectively gets "SMT core first, preprocessing tactics only when it returns unknown", which is what this PR does by hand: mkSimpleSolver is the same SMT core with no tactics. There are two differences:

• We create a fresh solver for each query, so we never enter incremental mode. That's why we pay for the tactics every time and have to ask for the simple solver ourselves.
• Z3 doesn't limit the incremental solver (solver2_timeout is UINT_MAX). We cap it with rlimit, because one query in liquidjava-example ran for 186 s in the simple solver before giving up. The default solver takes 0.4 s on that query.

We could also try auto-config false, as liquid-fixpoint does. I haven't measured it, so I'd leave it for a separate PR.