Z3's Spacer engine, running in your browser
warming up. Solving starts automatically.
A constrained Horn clause says: if these predicates hold and this constraint holds, then that predicate holds, or false. Program verification reduces to them. Unknown predicates stand for loop invariants and procedure summaries, and query clauses, with false in the head, encode the assertions.
In math notation, each line is a clause and its variables are universally quantified, with sorts inferred. Declare predicates with pred p(x: int). Operators are spelled as in Dafny or as symbols: && ∧, || ∨, ! ¬, ==> ⇒, != ≠, <= ≤. Comparisons chain, so 0 <= i < n works. Primed names like x' are ordinary variables, handy for next states. A head that isn't a predicate is the assertion. The toggle converts to and from SMT-LIB.
This page runs Z3's Spacer engine, compiled to WebAssembly, on clauses in the SMT-LIB format used by CHC-COMP. Sat means the clauses have a model. Its interpretations are invariants that prove every query unreachable, and each clause is re-checked under them in a fresh solver. Unsat means false is derivable, and the derivation is a concrete counterexample. It solves when you pause typing, with a 30-second limit. Z3's inlining of single-use predicates is switched off so every predicate you declare shows up in the answer.