Assertion violation at Simplex.h:130

[rainoftime]

Hi, for the following formula,

(set-logic QF_LIA)
(declare-fun v5 () Bool)
(declare-fun i3 () Int)
(declare-fun i4 () Int)
(assert (distinct (- (/ 55 93) i3) 96))
(assert (or (distinct (- (/ 55 93) i3) i4) v5))
(check-sat)

opensmt commit 134e367

opensmt: /home/opensmt/src/tsolvers/lasolver/Simplex.h:130: void Simplex::boundActivated(LVRef): Assertion `!tableau.isQuasiBasic(v) || boundsActivated[getVarId(v)] == 0' failed.
Aborted

[rainoftime]

(set-logic QF_LIA)
(declare-fun _substvar_122_ () Bool)
(declare-fun _substvar_129_ () Bool)
(declare-fun i2 () Int)
(declare-fun i3 () Int)
(assert (or _substvar_122_ (<= (- (* 734 i3)) 683)))
(assert (> 675 (- 734 i2)))
(assert (or (distinct 0.0 (+ (* 734 i3) i2)) _substvar_129_))
(check-sat)

[blishko]

Hi Jack!

Thanks for submitting these!
We are having an issue with our LIA solver which we plan to investigate this week.
It should address these new as well as some of the older issues you submitted.

[blishko]

Fixed by commit 46814dd in #111