AssertionError at Predef.scala:156 (ConjunctEliminator.scala:687)

[rainoftime]

Hi , for the following instance,

(set-logic HORN)
(declare-fun inv-int1 (Int Int) Bool)
(declare-fun inv-int2 (Int Int Int) Bool)
(declare-fun inv-int3 (Int Int Int Int) Bool)
(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const i1 Int)
(assert (forall ((q10 Int) (q11 Int) (q12 Bool)) (=> (distinct q12 q12 q12 q12) (<= q10 743))))
(assert (forall ((q13 Int) (q14 Int) (q15 Int) (q16 Int) (q17 Int) (q18 Int) (q19 Int) (q20 Int) (q21 Bool)) (=> (distinct q21 q21 q21 q21 q21) (= q20 583 583))))
(assert (forall ((q22 Int) (q23 Int) (q24 Bool)) (=> (<= (abs q23) (abs q23) q22) (and q24 q24 q24 q24 q24 q24 q24 q24))))
(assert (forall ((q25 Int) (q26 Bool)) (=> (distinct q26 q26 q26 q26 q26) (<= (div (mod q25 298) 335) (div (mod q25 298) 366) 366 (div (div 889 889) 889)))))
(assert (forall ((q44 Int) (q45 Int) (q46 Int) (q47 Int) (q48 Bool)) (=> (not q48) (> (div (mod q45 (div 143 415)) 415) 839 (mod q45 (div 143 415))))))
(declare-const i5 Int)
(assert (forall ((q49 Int) (q50 Int) (q51 Int) (q52 Bool)) (=> (= q51 (div q50 1000)) (or q52 q52))))
(assert (forall ((q56 Int) (q57 Int) (q58 Int) (q59 Int) (q60 Int) (q61 Int) (q62 Int) (q63 Bool)) (=> (not q63) (< 482 408))))
(assert (forall ((q64 Int) (q65 Int) (q66 Int) (q67 Int) (q68 Int) (q69 Int) (q70 Int) (q71 Int) (q72 Bool)) (=> (or q72 q72 q72 q72 q72 q72 q72) (> 248 q70))))
(assert (forall ((q73 Int) (q74 Int) (q75 Int) (q76 Int) (q77 Int) (q78 Int) (q79 Bool)) (=> (distinct q79 q79 q79 q79 q79 q79 q79 q79 q79) (> q78 945))))
(assert (forall ((q106 Int) (q107 Int) (q108 Int) (q109 Bool)) (=> (distinct q108 (- q107 q107 468 q107 468)) (and q109 q109 q109 q109 q109 q109))))
(assert (forall ((q110 Int) (q111 Int) (q112 Int) (q113 Int) (q114 Int) (q115 Int) (q116 Int) (q117 Bool)) (=> (<= (- q110 q116 q116 185 978) q116 q115 (- q110 q116 q116 185 978)) (or q117 q117 q117 q117))))
(check-sat)

Eldarica nightly (http://philipp.ruemmer.org/eldarica-bin-nightly.zip) throws an assertion error

 Theories: GroebnerMultiplication                                                                                                                                                                  [19/1822]
 Exception in thread "main" java.lang.AssertionError: assertion failed
        at scala.Predef$.assert(Predef.scala:156)
        at ap.terfor.conjunctions.ConjunctEliminator.eliminate(ConjunctEliminator.scala:687)
        at ap.terfor.conjunctions.ReduceWithConjunction$.constructConj(ReduceWithConjunction.scala:234)
        at ap.terfor.conjunctions.ReduceWithConjunction$.ap$terfor$conjunctions$ReduceWithConjunction$$reduceConj(ReduceWithConjunction.scala:100)
        at ap.terfor.conjunctions.ReduceWithConjunction.apply(ReduceWithConjunction.scala:420)
        at ap.terfor.conjunctions.ReduceWithConjunction.apply(ReduceWithConjunction.scala:413)
        at lazabs.horn.bottomup.HornPredAbs$.toInternal(HornPredAbs.scala:184)
        at lazabs.horn.bottomup.HornPredAbs$.toInternal(HornPredAbs.scala:172)
        at lazabs.horn.bottomup.HornClauses$$anon$2.instantiateConstraint(HornClauses.scala:413)
        at lazabs.horn.bottomup.HornPredAbs$NormClause$.apply(HornPredAbs.scala:378)
        at lazabs.horn.bottomup.HornPredAbs$$anonfun$38.apply(HornPredAbs.scala:616)
        at lazabs.horn.bottomup.HornPredAbs$$anonfun$38.apply(HornPredAbs.scala:614)

[pruemmer]

This should also be fixed in 2.0.4.