Convergence regression

[LeventErkok]

The following benchmark was quickly answered unsat with z3 compiled on March 3rd, 2025. It diverges with a freshly compiled z3. @levnach I'm wondering if it might have something to do with the recent GCD related changes since it uses the divisibility predicate.

(set-option :smtlib2_compliant true)
(set-option :print-success false)
(set-option :global-declarations true)
(set-option :produce-models true)
(set-logic ALL) ; has unbounded values, using catch-all.
(define-fun s8 () Int 2)
(define-fun s16 () Int 4)
(declare-fun s0 () Int)
(declare-fun s5 () Int)
(declare-fun k () Int)
(define-fun s1 () Bool ((_ divisible 2) s0))
(define-fun s2 () Int (* s0 s0))
(define-fun s3 () Bool ((_ divisible 4) s2))
(define-fun s4 () Bool (=> s1 s3))
(define-fun s6 () Bool ((_ divisible 2) s5))
(define-fun s7 () Int (* s5 s5))
(define-fun s9 () Int k)
(define-fun s10 () Bool (exists ((l1_s0 Int))
                          (let ((l1_s1 2))
                          (let ((l1_s2 (* l1_s0 l1_s1)))
                          (let ((l1_s3 (= s5 l1_s2)))
                          l1_s3)))))
(define-fun s11 () Int (* s8 s9))
(define-fun s12 () Bool (= s5 s11))
(define-fun s13 () Bool (=> s10 s12))
(define-fun s14 () Int (* s11 s11))
(define-fun s15 () Bool (= s7 s14))
(define-fun s17 () Int (* s9 s9))
(define-fun s18 () Int (* s16 s17))
(define-fun s19 () Bool (= s14 s18))
(define-fun s20 () Bool (= s7 s18))
(assert s13)
(push 1)
(define-fun s23 () Bool (not s19))
(assert s23)
(check-sat)
(pop 1)
(push 1)
(define-fun s24 () Bool (=> s6 s20))
(define-fun s25 () Bool (=> s6 s24))
(assert s25)
(define-fun s26 () Bool ((_ divisible 4) s7))
(define-fun s27 () Bool (=> s6 s26))
(define-fun s28 () Bool (not s27))
(assert s28)
(check-sat)

[levnach]

@LeventErkok , thank you for reporting. I am seeing the regression and going to try fixing it. To restore the previous behavior of z3 please run it with option lp.dio=false.

[levnach]

I think it is fixed by a1673f2. The benchmark is solved with the default options.

[LeventErkok]

Thanks for the quick fix @levnach! I can confirm that your commit fixes the issue. Much appreciated.