Which solver should I choose? llrêve reduces the problem of checking the programs for equivalence to a set of SMT clauses. These clauses are then passed to an SMT solver. You can select two different SMT solvers in the webinterface, namely Z3 and Eldarica. You can choose between two separate inference engines built into Z3 (called duality and spacer). In addition to that you can also choose Dynamic invariant inference. In this case llrêve tries to infer invariants by executing the two programs and analyzing these execution traces. The task of checking whether these invariants hold and whether they are strong enough to prove equivalence is delegated to Z3. Finally you can also choose the Race-option. In this case Z3, Eldarica and the dynamic invariant inference are started in parallel and the result of the fastest procedure is returned.

How do I specify invariant patterns? Each line represents one pattern and needs to be terminated by ;. Available operators /\ boolean conjunction \/ boolean disjunction +,-,* addition, subtraction, multiplication _ Hole that will be instantiated using available variables <,<=,=,>=,> integer comparisons