Debug branch: ASSERTION VIOLATION File: ../src/math/lp/nla_core.cpp Line: 441 !ineq_holds(ineq(cmp, t, rs))

[wintered]

Hi,
For this formula:

(assert
 (exists ((b Int) (c Int) (a Real) (d Int))
  (and (< b (* 114 a (- 228 (- 195 221 176) c) (* 158 (- 176) d)))
   (>= b (* 113 150 (- 50 29 a) (- 68 (/ 106 129 6) c) (* 232 (* 222 94 42) d))))))
(check-sat)

Z3 throws out an assertion violation:

ASSERTION VIOLATION
File: ../src/math/lp/nla_core.cpp
Line: 441
!ineq_holds(ineq(cmp, t, rs))
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB

OS: Ubuntu 18.04
Commit: 794c094 (debug branch)

[levnach]

It does not reproduce anymore. The problem is solved often in a short time depending on the random seed.

[zhendongsu]

It still reproduces for me on the latest debug branch with the following very similar test:

[513] % z3debug small.smt2 
ASSERTION VIOLATION
File: ../src/math/lp/nla_core.cpp
Line: 441
!ineq_holds(ineq(cmp, t, rs))
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
[514] % 
[514] % cat small.smt2 
(assert
 (exists ((x Int) (y Int) (a Real) (z Int))
  (or (< x (* 114 a (- 228 (- 195 10 113) y) (* 158 (- 176 64 93) z)))
   (>= x (* 113 46 (- 50 6 a) (- 68 (/ 106 224 43) y) (* 232 (* 222 82 157) z))))))
(check-sat)
[515] % 

[NikolajBjorner]

metoo

[NikolajBjorner]

Seems it was now fixed. The solver diverges instead.