merlin

Refutation unsoundness issue: ``` $ z3 tactic.default_tactic=smt sat.euf=true small.smt2 unsat $ z3 small.smt2 sat $ cat small.smt2 (declare-fun v () (Array Bool Int)) (declare-fun a () Bool) (declare-fun va ()...

``` $ cat small.smt2 (declare-const x Bool) (declare-fun b (Int Int Real) (Array Int (Array Int Real))) (declare-fun b (Int Int) Int) (declare-fun v () Bool) (declare-fun a () Int)...

Another case potentially relevant to https://github.com/Z3Prover/z3/issues/7027#issuecomment-2094557908 ``` $ z3 tactic.default_tactic=smt sat.euf=true small.smt2 unsat $ z3 small.smt2 sat $ cat small.smt2 (declare-fun v () (Array Bool Int)) (declare-fun a () Bool)...

``` $ z3 tactic.default_tactic=smt sat.euf=true small.smt2 ASSERTION VIOLATION File: ../src/sat/smt/pb_solver.cpp Line: 3467 Failed to verify: this == sat::constraint_base::to_extension(index) $ cat small.smt2 (declare-fun ar4 () Int) (declare-fun r41 () Int) (declare-fun...

``` $ cat small.smt2 (declare-const v (_ BitVec 7)) (declare-const x (_ FloatingPoint 2 6)) (assert (or true (fp.eq x ((_ to_fp 2 6) ((_ zero_extend 1) v))))) (check-sat-using (then...

Another case: ``` $ cat case.smt2 (declare-const x Bool) (declare-fun v () (Seq (Seq Int))) (assert (forall ((a (Seq Int)) (va (Seq (Seq Int)))) (and (not x) (distinct v (seq.++...

A related instance: ``` $ cat delta.smt2 (declare-fun v () Int) (declare-fun a () String) (assert (or (distinct (str.substr a 0 0) (str.substr a 0 0)) (= (div 1 0)...

https://github.com/Z3Prover/z3/commit/2c8df54b70f5456efd0b2c3f4917d2b314098f19 ``` $ z3 small.smt2 unsat sat $ cat small.smt2 (declare-fun a () (Array (_ BitVec 1) (_ BitVec 1))) (assert (distinct false (exists ((r (Array (_ BitVec 1) (_...

I noticed that the issue has already been resolved by the PR. Thank you for addressing it!

Thank you, @jhoenicke ! That's very helpful. I will try out the latest version of SMTInterpol. I also look forward to hearing more about your great work in the future....