search

ultimate-pa / smtinterpol

SMTInterpol interpolating SMT solver
GNU Lesser General Public License v3.0
61 stars 17 forks source link

Assertion error at SMTAffineTerm.java:83 on HORN formula #117

Closed rainoftime closed 5 months ago

rainoftime commented 4 years ago

Hi, for the following formula

(set-logic HORN)
(declare-fun ULTIMATE.start_L7 (Int Int Int Int Int Int Int Int Bool) Bool)
(declare-fun ULTIMATE.start_L23 (Int Int Int Int Int Int Int Int Bool) Bool)
(declare-fun ULTIMATE.start_ULTIMATE.startFINAL (Int Int Int Int Int Int Int Int Bool) Bool)
(declare-fun ULTIMATE.start_L-1 (Int Int Int Int Int Int Int Int Bool) Bool)
(declare-fun ULTIMATE.start_L5 (Int Int Int Int Int Int Int Int Bool) Bool)
(declare-fun ULTIMATE.start_L29 (Int Int Int Int Int Int Int Int Bool) Bool)
(declare-fun ULTIMATE.start_ULTIMATE.startENTRY (Int Int Int Int Int Int Int Int Bool) Bool)
(declare-fun ULTIMATE.start_L17 (Int Int Int Int Int Int Int Int Bool) Bool)
(declare-fun ULTIMATE.start_ULTIMATE.startEXIT (Int Int Int Int Int Int Int Int Bool) Bool)
(assert (forall ((hhv_ULTIMATE.start_L-1_0_Int Int) (hhv_ULTIMATE.start_L-1_1_Int Int) (hhv_ULTIMATE.start_L-1_2_Int Int) (hhv_ULTIMATE.start_L-1_3_Int Int) (hhv_ULTIMATE.start_L-1_4_Int Int) (hhv_ULTIMATE.start_L-1_5_Int Int) (hhv_ULTIMATE.start_L-1_6_Int Int) (hhv_ULTIMATE.start_L-1_7_Int Int) (hhv_ULTIMATE.start_L-1_8_Bool Bool) (hbv_ULTIMATE.start_ULTIMATE.startENTRY_0_Int Int) (hbv_ULTIMATE.start_ULTIMATE.startENTRY_1_Int Int) (hbv_ULTIMATE.start_ULTIMATE.startENTRY_2_Int Int) (hbv_ULTIMATE.start_ULTIMATE.startENTRY_3_Int Int) (hbv_ULTIMATE.start_ULTIMATE.startENTRY_4_Int Int) (hbv_ULTIMATE.start_ULTIMATE.startENTRY_5_Int Int) (hbv_ULTIMATE.start_ULTIMATE.startENTRY_6_Int Int) (hbv_ULTIMATE.start_ULTIMATE.startENTRY_7_Int Int) (hbv_ULTIMATE.start_ULTIMATE.startENTRY_8_Bool Bool)) (=> (and (or (= hhv_ULTIMATE.start_L-1_0_Int 0) hhv_ULTIMATE.start_L-1_8_Bool) (ULTIMATE.start_ULTIMATE.startENTRY hbv_ULTIMATE.start_ULTIMATE.startENTRY_0_Int hhv_ULTIMATE.start_L-1_1_Int hhv_ULTIMATE.start_L-1_2_Int hhv_ULTIMATE.start_L-1_3_Int hhv_ULTIMATE.start_L-1_4_Int hhv_ULTIMATE.start_L-1_5_Int hhv_ULTIMATE.start_L-1_6_Int hhv_ULTIMATE.start_L-1_7_Int hhv_ULTIMATE.start_L-1_8_Bool)) (ULTIMATE.start_L-1 hhv_ULTIMATE.start_L-1_0_Int hhv_ULTIMATE.start_L-1_1_Int hhv_ULTIMATE.start_L-1_2_Int hhv_ULTIMATE.start_L-1_3_Int hhv_ULTIMATE.start_L-1_4_Int hhv_ULTIMATE.start_L-1_5_Int hhv_ULTIMATE.start_L-1_6_Int hhv_ULTIMATE.start_L-1_7_Int hhv_ULTIMATE.start_L-1_8_Bool))))
(assert (forall ((hhv_ULTIMATE.start_L17_0_Int Int) (hhv_ULTIMATE.start_L17_1_Int Int) (hhv_ULTIMATE.start_L17_2_Int Int) (hhv_ULTIMATE.start_L17_3_Int Int) (hhv_ULTIMATE.start_L17_4_Int Int) (hhv_ULTIMATE.start_L17_5_Int Int) (hhv_ULTIMATE.start_L17_6_Int Int) (hhv_ULTIMATE.start_L17_7_Int Int) (hhv_ULTIMATE.start_L17_8_Bool Bool) (hbv_ULTIMATE.start_L-1_0_Int Int) (hbv_ULTIMATE.start_L-1_1_Int Int) (hbv_ULTIMATE.start_L-1_2_Int Int) (hbv_ULTIMATE.start_L-1_3_Int Int) (hbv_ULTIMATE.start_L-1_4_Int Int) (hbv_ULTIMATE.start_L-1_5_Int Int) (hbv_ULTIMATE.start_L-1_6_Int Int) (hbv_ULTIMATE.start_L-1_7_Int Int) (hbv_ULTIMATE.start_L-1_8_Bool Bool)) (=> (and (ULTIMATE.start_L-1 hhv_ULTIMATE.start_L17_0_Int hhv_ULTIMATE.start_L17_1_Int hhv_ULTIMATE.start_L17_2_Int hbv_ULTIMATE.start_L-1_3_Int hbv_ULTIMATE.start_L-1_4_Int hbv_ULTIMATE.start_L-1_5_Int hbv_ULTIMATE.start_L-1_6_Int hbv_ULTIMATE.start_L-1_7_Int hhv_ULTIMATE.start_L17_8_Bool) (or hhv_ULTIMATE.start_L17_8_Bool (and (= hhv_ULTIMATE.start_L17_6_Int (- 3)) (= hhv_ULTIMATE.start_L17_5_Int hhv_ULTIMATE.start_L17_6_Int)))) (ULTIMATE.start_L17 hhv_ULTIMATE.start_L17_0_Int hhv_ULTIMATE.start_L17_1_Int hhv_ULTIMATE.start_L17_2_Int hhv_ULTIMATE.start_L17_3_Int hhv_ULTIMATE.start_L17_4_Int hhv_ULTIMATE.start_L17_5_Int hhv_ULTIMATE.start_L17_6_Int hhv_ULTIMATE.start_L17_7_Int hhv_ULTIMATE.start_L17_8_Bool))))
(assert (forall ((hhv_ULTIMATE.start_L23_0_Int Int) (hhv_ULTIMATE.start_L23_1_Int Int) (hhv_ULTIMATE.start_L23_2_Int Int) (hhv_ULTIMATE.start_L23_3_Int Int) (hhv_ULTIMATE.start_L23_4_Int Int) (hhv_ULTIMATE.start_L23_5_Int Int) (hhv_ULTIMATE.start_L23_6_Int Int) (hhv_ULTIMATE.start_L23_7_Int Int) (hhv_ULTIMATE.start_L23_8_Bool Bool) (hbv_ULTIMATE.start_L17_0_Int Int) (hbv_ULTIMATE.start_L17_1_Int Int) (hbv_ULTIMATE.start_L17_2_Int Int) (hbv_ULTIMATE.start_L17_3_Int Int) (hbv_ULTIMATE.start_L17_4_Int Int) (hbv_ULTIMATE.start_L17_5_Int Int) (hbv_ULTIMATE.start_L17_6_Int Int) (hbv_ULTIMATE.start_L17_7_Int Int) (hbv_ULTIMATE.start_L17_8_Bool Bool)) (=> (and (or (and (= hhv_ULTIMATE.start_L23_3_Int (- hhv_ULTIMATE.start_L23_5_Int)) (< hhv_ULTIMATE.start_L23_5_Int 0)) hhv_ULTIMATE.start_L23_8_Bool) (ULTIMATE.start_L17 hhv_ULTIMATE.start_L23_0_Int hhv_ULTIMATE.start_L23_1_Int hhv_ULTIMATE.start_L23_2_Int hbv_ULTIMATE.start_L17_3_Int hhv_ULTIMATE.start_L23_4_Int hhv_ULTIMATE.start_L23_5_Int hhv_ULTIMATE.start_L23_6_Int hhv_ULTIMATE.start_L23_7_Int hhv_ULTIMATE.start_L23_8_Bool)) (ULTIMATE.start_L23 hhv_ULTIMATE.start_L23_0_Int hhv_ULTIMATE.start_L23_1_Int hhv_ULTIMATE.start_L23_2_Int hhv_ULTIMATE.start_L23_3_Int hhv_ULTIMATE.start_L23_4_Int hhv_ULTIMATE.start_L23_5_Int hhv_ULTIMATE.start_L23_6_Int hhv_ULTIMATE.start_L23_7_Int hhv_ULTIMATE.start_L23_8_Bool))))
(assert (forall ((hhv_ULTIMATE.start_L23_0_Int Int) (hhv_ULTIMATE.start_L23_1_Int Int) (hhv_ULTIMATE.start_L23_2_Int Int) (hhv_ULTIMATE.start_L23_3_Int Int) (hhv_ULTIMATE.start_L23_4_Int Int) (hhv_ULTIMATE.start_L23_5_Int Int) (hhv_ULTIMATE.start_L23_6_Int Int) (hhv_ULTIMATE.start_L23_7_Int Int) (hhv_ULTIMATE.start_L23_8_Bool Bool) (hbv_ULTIMATE.start_L17_0_Int Int) (hbv_ULTIMATE.start_L17_1_Int Int) (hbv_ULTIMATE.start_L17_2_Int Int) (hbv_ULTIMATE.start_L17_3_Int Int) (hbv_ULTIMATE.start_L17_4_Int Int) (hbv_ULTIMATE.start_L17_5_Int Int) (hbv_ULTIMATE.start_L17_6_Int Int) (hbv_ULTIMATE.start_L17_7_Int Int) (hbv_ULTIMATE.start_L17_8_Bool Bool)) (=> (and (ULTIMATE.start_L17 hhv_ULTIMATE.start_L23_0_Int hhv_ULTIMATE.start_L23_1_Int hhv_ULTIMATE.start_L23_2_Int hbv_ULTIMATE.start_L17_3_Int hhv_ULTIMATE.start_L23_4_Int hhv_ULTIMATE.start_L23_5_Int hhv_ULTIMATE.start_L23_6_Int hhv_ULTIMATE.start_L23_7_Int hhv_ULTIMATE.start_L23_8_Bool) (or (and (= hhv_ULTIMATE.start_L23_3_Int hhv_ULTIMATE.start_L23_5_Int) (not (< hhv_ULTIMATE.start_L23_5_Int 0))) hhv_ULTIMATE.start_L23_8_Bool)) (ULTIMATE.start_L23 hhv_ULTIMATE.start_L23_0_Int hhv_ULTIMATE.start_L23_1_Int hhv_ULTIMATE.start_L23_2_Int hhv_ULTIMATE.start_L23_3_Int hhv_ULTIMATE.start_L23_4_Int hhv_ULTIMATE.start_L23_5_Int hhv_ULTIMATE.start_L23_6_Int hhv_ULTIMATE.start_L23_7_Int hhv_ULTIMATE.start_L23_8_Bool))))
(assert (forall ((hhv_ULTIMATE.start_L29_0_Int Int) (hhv_ULTIMATE.start_L29_1_Int Int) (hhv_ULTIMATE.start_L29_2_Int Int) (hhv_ULTIMATE.start_L29_3_Int Int) (hhv_ULTIMATE.start_L29_4_Int Int) (hhv_ULTIMATE.start_L29_5_Int Int) (hhv_ULTIMATE.start_L29_6_Int Int) (hhv_ULTIMATE.start_L29_7_Int Int) (hhv_ULTIMATE.start_L29_8_Bool Bool) (hbv_ULTIMATE.start_L23_0_Int Int) (hbv_ULTIMATE.start_L23_1_Int Int) (hbv_ULTIMATE.start_L23_2_Int Int) (hbv_ULTIMATE.start_L23_3_Int Int) (hbv_ULTIMATE.start_L23_4_Int Int) (hbv_ULTIMATE.start_L23_5_Int Int) (hbv_ULTIMATE.start_L23_6_Int Int) (hbv_ULTIMATE.start_L23_7_Int Int) (hbv_ULTIMATE.start_L23_8_Bool Bool)) (=> (and (or (and (<= 0 (+ hhv_ULTIMATE.start_L29_3_Int 2147483648)) (= hhv_ULTIMATE.start_L29_3_Int hhv_ULTIMATE.start_L29_0_Int) (<= hhv_ULTIMATE.start_L29_3_Int 2147483647)) hhv_ULTIMATE.start_L29_8_Bool) (ULTIMATE.start_L23 hbv_ULTIMATE.start_L23_0_Int hhv_ULTIMATE.start_L29_1_Int hhv_ULTIMATE.start_L29_2_Int hhv_ULTIMATE.start_L29_3_Int hhv_ULTIMATE.start_L29_4_Int hhv_ULTIMATE.start_L29_5_Int hhv_ULTIMATE.start_L29_6_Int hbv_ULTIMATE.start_L23_7_Int hhv_ULTIMATE.start_L29_8_Bool)) (ULTIMATE.start_L29 hhv_ULTIMATE.start_L29_0_Int hhv_ULTIMATE.start_L29_1_Int hhv_ULTIMATE.start_L29_2_Int hhv_ULTIMATE.start_L29_3_Int hhv_ULTIMATE.start_L29_4_Int hhv_ULTIMATE.start_L29_5_Int hhv_ULTIMATE.start_L29_6_Int hhv_ULTIMATE.start_L29_7_Int hhv_ULTIMATE.start_L29_8_Bool))))
(assert (forall ((hhv_ULTIMATE.start_L5_0_Int Int) (hhv_ULTIMATE.start_L5_1_Int Int) (hhv_ULTIMATE.start_L5_2_Int Int) (hhv_ULTIMATE.start_L5_3_Int Int) (hhv_ULTIMATE.start_L5_4_Int Int) (hhv_ULTIMATE.start_L5_5_Int Int) (hhv_ULTIMATE.start_L5_6_Int Int) (hhv_ULTIMATE.start_L5_7_Int Int) (hhv_ULTIMATE.start_L5_8_Bool Bool) (hbv_ULTIMATE.start_L29_0_Int Int) (hbv_ULTIMATE.start_L29_1_Int Int) (hbv_ULTIMATE.start_L29_2_Int Int) (hbv_ULTIMATE.start_L29_3_Int Int) (hbv_ULTIMATE.start_L29_4_Int Int) (hbv_ULTIMATE.start_L29_5_Int Int) (hbv_ULTIMATE.start_L29_6_Int Int) (hbv_ULTIMATE.start_L29_7_Int Int) (hbv_ULTIMATE.start_L29_8_Bool Bool)) (=> (and (or hhv_ULTIMATE.start_L5_8_Bool (<= 0 hhv_ULTIMATE.start_L5_0_Int)) (ULTIMATE.start_L29 hhv_ULTIMATE.start_L5_0_Int hhv_ULTIMATE.start_L5_1_Int hhv_ULTIMATE.start_L5_2_Int hhv_ULTIMATE.start_L5_3_Int hhv_ULTIMATE.start_L5_4_Int hhv_ULTIMATE.start_L5_5_Int hhv_ULTIMATE.start_L5_6_Int hhv_ULTIMATE.start_L5_7_Int hhv_ULTIMATE.start_L5_8_Bool)) (ULTIMATE.start_L5 hhv_ULTIMATE.start_L5_0_Int hhv_ULTIMATE.start_L5_1_Int hhv_ULTIMATE.start_L5_2_Int hhv_ULTIMATE.start_L5_3_Int hhv_ULTIMATE.start_L5_4_Int hhv_ULTIMATE.start_L5_5_Int hhv_ULTIMATE.start_L5_6_Int hhv_ULTIMATE.start_L5_7_Int hhv_ULTIMATE.start_L5_8_Bool))))
(assert (forall ((hhv_ULTIMATE.start_L7_0_Int Int) (hhv_ULTIMATE.start_L7_1_Int Int) (hhv_ULTIMATE.start_L7_2_Int Int) (hhv_ULTIMATE.start_L7_3_Int Int) (hhv_ULTIMATE.start_L7_4_Int Int) (hhv_ULTIMATE.start_L7_5_Int Int) (hhv_ULTIMATE.start_L7_6_Int Int) (hhv_ULTIMATE.start_L7_7_Int Int) (hhv_ULTIMATE.start_L7_8_Bool Bool) (hbv_ULTIMATE.start_L29_0_Int Int) (hbv_ULTIMATE.start_L29_1_Int Int) (hbv_ULTIMATE.start_L29_2_Int Int) (hbv_ULTIMATE.start_L29_3_Int Int) (hbv_ULTIMATE.start_L29_4_Int Int) (hbv_ULTIMATE.start_L29_5_Int Int) (hbv_ULTIMATE.start_L29_6_Int Int) (hbv_ULTIMATE.start_L29_7_Int Int) (hbv_ULTIMATE.start_L29_8_Bool Bool)) (=> (and (ULTIMATE.start_L29 hhv_ULTIMATE.start_L7_0_Int hhv_ULTIMATE.start_L7_1_Int hhv_ULTIMATE.start_L7_2_Int hhv_ULTIMATE.start_L7_3_Int hhv_ULTIMATE.start_L7_4_Int hhv_ULTIMATE.start_L7_5_Int hhv_ULTIMATE.start_L7_6_Int hhv_ULTIMATE.start_L7_7_Int hhv_ULTIMATE.start_L7_8_Bool) (or (not (<= 0 hhv_ULTIMATE.start_L7_0_Int)) hhv_ULTIMATE.start_L7_8_Bool)) (ULTIMATE.start_L7 hhv_ULTIMATE.start_L7_0_Int hhv_ULTIMATE.start_L7_1_Int hhv_ULTIMATE.start_L7_2_Int hhv_ULTIMATE.start_L7_3_Int hhv_ULTIMATE.start_L7_4_Int hhv_ULTIMATE.start_L7_5_Int hhv_ULTIMATE.start_L7_6_Int hhv_ULTIMATE.start_L7_7_Int hhv_ULTIMATE.start_L7_8_Bool))))
(assert (forall ((hhv_ULTIMATE.start_ULTIMATE.startFINAL_0_Int Int) (hhv_ULTIMATE.start_ULTIMATE.startFINAL_1_Int Int) (hhv_ULTIMATE.start_ULTIMATE.startFINAL_2_Int Int) (hhv_ULTIMATE.start_ULTIMATE.startFINAL_3_Int Int) (hhv_ULTIMATE.start_ULTIMATE.startFINAL_4_Int Int) (hhv_ULTIMATE.start_ULTIMATE.startFINAL_5_Int Int) (hhv_ULTIMATE.start_ULTIMATE.startFINAL_6_Int Int) (hhv_ULTIMATE.start_ULTIMATE.startFINAL_7_Int Int) (hhv_ULTIMATE.start_ULTIMATE.startFINAL_8_Bool Bool) (hbv_ULTIMATE.start_L5_0_Int Int) (hbv_ULTIMATE.start_L5_1_Int Int) (hbv_ULTIMATE.start_L5_2_Int Int) (hbv_ULTIMATE.start_L5_3_Int Int) (hbv_ULTIMATE.start_L5_4_Int Int) (hbv_ULTIMATE.start_L5_5_Int Int) (hbv_ULTIMATE.start_L5_6_Int Int) (hbv_ULTIMATE.start_L5_7_Int Int) (hbv_ULTIMATE.start_L5_8_Bool Bool)) (=> (and (or hhv_ULTIMATE.start_ULTIMATE.startFINAL_8_Bool (= hhv_ULTIMATE.start_ULTIMATE.startFINAL_2_Int hhv_ULTIMATE.start_ULTIMATE.startFINAL_4_Int)) (ULTIMATE.start_L5 hhv_ULTIMATE.start_ULTIMATE.startFINAL_0_Int hhv_ULTIMATE.start_ULTIMATE.startFINAL_1_Int hbv_ULTIMATE.start_L5_2_Int hhv_ULTIMATE.start_ULTIMATE.startFINAL_3_Int hhv_ULTIMATE.start_ULTIMATE.startFINAL_4_Int hhv_ULTIMATE.start_ULTIMATE.startFINAL_5_Int hhv_ULTIMATE.start_ULTIMATE.startFINAL_6_Int hhv_ULTIMATE.start_ULTIMATE.startFINAL_7_Int hhv_ULTIMATE.start_ULTIMATE.startFINAL_8_Bool)) (ULTIMATE.start_ULTIMATE.startFINAL hhv_ULTIMATE.start_ULTIMATE.startFINAL_0_Int hhv_ULTIMATE.start_ULTIMATE.startFINAL_1_Int hhv_ULTIMATE.start_ULTIMATE.startFINAL_2_Int hhv_ULTIMATE.start_ULTIMATE.startFINAL_3_Int hhv_ULTIMATE.start_ULTIMATE.startFINAL_4_Int hhv_ULTIMATE.start_ULTIMATE.startFINAL_5_Int hhv_ULTIMATE.start_ULTIMATE.startFINAL_6_Int hhv_ULTIMATE.start_ULTIMATE.startFINAL_7_Int hhv_ULTIMATE.start_ULTIMATE.startFINAL_8_Bool))))
(assert (forall ((hhv_ULTIMATE.start_ULTIMATE.startEXIT_0_Int Int) (hhv_ULTIMATE.start_ULTIMATE.startEXIT_1_Int Int) (hhv_ULTIMATE.start_ULTIMATE.startEXIT_2_Int Int) (hhv_ULTIMATE.start_ULTIMATE.startEXIT_3_Int Int) (hhv_ULTIMATE.start_ULTIMATE.startEXIT_4_Int Int) (hhv_ULTIMATE.start_ULTIMATE.startEXIT_5_Int Int) (hhv_ULTIMATE.start_ULTIMATE.startEXIT_6_Int Int) (hhv_ULTIMATE.start_ULTIMATE.startEXIT_7_Int Int) (hhv_ULTIMATE.start_ULTIMATE.startEXIT_8_Bool Bool) (hbv_ULTIMATE.start_L7_0_Int Int) (hbv_ULTIMATE.start_L7_1_Int Int) (hbv_ULTIMATE.start_L7_2_Int Int) (hbv_ULTIMATE.start_L7_3_Int Int) (hbv_ULTIMATE.start_L7_4_Int Int) (hbv_ULTIMATE.start_L7_5_Int Int) (hbv_ULTIMATE.start_L7_6_Int Int) (hbv_ULTIMATE.start_L7_7_Int Int) (hbv_ULTIMATE.start_L7_8_Bool Bool)) (=> (and (ULTIMATE.start_L7 hhv_ULTIMATE.start_ULTIMATE.startEXIT_0_Int hhv_ULTIMATE.start_ULTIMATE.startEXIT_1_Int hhv_ULTIMATE.start_ULTIMATE.startEXIT_2_Int hhv_ULTIMATE.start_ULTIMATE.startEXIT_3_Int hhv_ULTIMATE.start_ULTIMATE.startEXIT_4_Int hhv_ULTIMATE.start_ULTIMATE.startEXIT_5_Int hhv_ULTIMATE.start_ULTIMATE.startEXIT_6_Int hhv_ULTIMATE.start_ULTIMATE.startEXIT_7_Int hbv_ULTIMATE.start_L7_8_Bool) hhv_ULTIMATE.start_ULTIMATE.startEXIT_8_Bool) (ULTIMATE.start_ULTIMATE.startEXIT hhv_ULTIMATE.start_ULTIMATE.startEXIT_0_Int hhv_ULTIMATE.start_ULTIMATE.startEXIT_1_Int hhv_ULTIMATE.start_ULTIMATE.startEXIT_2_Int hhv_ULTIMATE.start_ULTIMATE.startEXIT_3_Int hhv_ULTIMATE.start_ULTIMATE.startEXIT_4_Int hhv_ULTIMATE.start_ULTIMATE.startEXIT_5_Int hhv_ULTIMATE.start_ULTIMATE.startEXIT_6_Int hhv_ULTIMATE.start_ULTIMATE.startEXIT_7_Int hhv_ULTIMATE.start_ULTIMATE.startEXIT_8_Bool))))
(assert (forall ((hhv_ULTIMATE.start_L5_0_Int Int) (hhv_ULTIMATE.start_L5_1_Int Int) (hhv_ULTIMATE.start_L5_2_Int Int) (hhv_ULTIMATE.start_L5_3_Int Int) (hhv_ULTIMATE.start_L5_4_Int Int) (hhv_ULTIMATE.start_L5_5_Int Int) (hhv_ULTIMATE.start_L5_6_Int Int) (hhv_ULTIMATE.start_L5_7_Int Int) (hhv_ULTIMATE.start_L5_8_Bool Bool) (hbv_ULTIMATE.start_L7_0_Int Int) (hbv_ULTIMATE.start_L7_1_Int Int) (hbv_ULTIMATE.start_L7_2_Int Int) (hbv_ULTIMATE.start_L7_3_Int Int) (hbv_ULTIMATE.start_L7_4_Int Int) (hbv_ULTIMATE.start_L7_5_Int Int) (hbv_ULTIMATE.start_L7_6_Int Int) (hbv_ULTIMATE.start_L7_7_Int Int) (hbv_ULTIMATE.start_L7_8_Bool Bool)) (=> (and hhv_ULTIMATE.start_L5_8_Bool (ULTIMATE.start_L7 hhv_ULTIMATE.start_L5_0_Int hhv_ULTIMATE.start_L5_1_Int hhv_ULTIMATE.start_L5_2_Int hhv_ULTIMATE.start_L5_3_Int hhv_ULTIMATE.start_L5_4_Int hhv_ULTIMATE.start_L5_5_Int hhv_ULTIMATE.start_L5_6_Int hhv_ULTIMATE.start_L5_7_Int hhv_ULTIMATE.start_L5_8_Bool)) (ULTIMATE.start_L5 hhv_ULTIMATE.start_L5_0_Int hhv_ULTIMATE.start_L5_1_Int hhv_ULTIMATE.start_L5_2_Int hhv_ULTIMATE.start_L5_3_Int hhv_ULTIMATE.start_L5_4_Int hhv_ULTIMATE.start_L5_5_Int hhv_ULTIMATE.start_L5_6_Int hhv_ULTIMATE.start_L5_7_Int hhv_ULTIMATE.start_L5_8_Bool))))
(assert (forall ((hhv_ULTIMATE.start_ULTIMATE.startEXIT_0_Int Int) (hhv_ULTIMATE.start_ULTIMATE.startEXIT_1_Int Int) (hhv_ULTIMATE.start_ULTIMATE.startEXIT_2_Int Int) (hhv_ULTIMATE.start_ULTIMATE.startEXIT_3_Int Int) (hhv_ULTIMATE.start_ULTIMATE.startEXIT_4_Int Int) (hhv_ULTIMATE.start_ULTIMATE.startEXIT_5_Int Int) (hhv_ULTIMATE.start_ULTIMATE.startEXIT_6_Int Int) (hhv_ULTIMATE.start_ULTIMATE.startEXIT_7_Int Int) (hhv_ULTIMATE.start_ULTIMATE.startEXIT_8_Bool Bool) (hbv_ULTIMATE.start_ULTIMATE.startFINAL_0_Int Int) (hbv_ULTIMATE.start_ULTIMATE.startFINAL_1_Int Int) (hbv_ULTIMATE.start_ULTIMATE.startFINAL_2_Int Int) (hbv_ULTIMATE.start_ULTIMATE.startFINAL_3_Int Int) (hbv_ULTIMATE.start_ULTIMATE.startFINAL_4_Int Int) (hbv_ULTIMATE.start_ULTIMATE.startFINAL_5_Int Int) (hbv_ULTIMATE.start_ULTIMATE.startFINAL_6_Int Int) (hbv_ULTIMATE.start_ULTIMATE.startFINAL_7_Int Int) (hbv_ULTIMATE.start_ULTIMATE.startFINAL_8_Bool Bool)) (=> (ULTIMATE.start_ULTIMATE.startFINAL hhv_ULTIMATE.start_ULTIMATE.startEXIT_0_Int hhv_ULTIMATE.start_ULTIMATE.startEXIT_1_Int hhv_ULTIMATE.start_ULTIMATE.startEXIT_2_Int hhv_ULTIMATE.start_ULTIMATE.startEXIT_3_Int hhv_ULTIMATE.start_ULTIMATE.startEXIT_4_Int hhv_ULTIMATE.start_ULTIMATE.startEXIT_5_Int hhv_ULTIMATE.start_ULTIMATE.startEXIT_6_Int hhv_ULTIMATE.start_ULTIMATE.startEXIT_7_Int hhv_ULTIMATE.start_ULTIMATE.startEXIT_8_Bool) (ULTIMATE.start_ULTIMATE.startEXIT hhv_ULTIMATE.start_ULTIMATE.startEXIT_0_Int hhv_ULTIMATE.start_ULTIMATE.startEXIT_1_Int hhv_ULTIMATE.start_ULTIMATE.startEXIT_2_Int hhv_ULTIMATE.start_ULTIMATE.startEXIT_3_Int hhv_ULTIMATE.start_ULTIMATE.startEXIT_4_Int hhv_ULTIMATE.start_ULTIMATE.startEXIT_5_Int hhv_ULTIMATE.start_ULTIMATE.startEXIT_6_Int hhv_ULTIMATE.start_ULTIMATE.startEXIT_7_Int hhv_ULTIMATE.start_ULTIMATE.startEXIT_8_Bool))))
(assert (forall ((hhv_ULTIMATE.start_ULTIMATE.startEXIT_0_Int Int) (hhv_ULTIMATE.start_ULTIMATE.startEXIT_1_Int Int) (hhv_ULTIMATE.start_ULTIMATE.startEXIT_2_Int Int) (hhv_ULTIMATE.start_ULTIMATE.startEXIT_3_Int Int) (hhv_ULTIMATE.start_ULTIMATE.startEXIT_4_Int Int) (hhv_ULTIMATE.start_ULTIMATE.startEXIT_5_Int Int) (hhv_ULTIMATE.start_ULTIMATE.startEXIT_6_Int Int) (hhv_ULTIMATE.start_ULTIMATE.startEXIT_7_Int Int) (hhv_ULTIMATE.start_ULTIMATE.startEXIT_8_Bool Bool) (hbv_ULTIMATE.start_ULTIMATE.startFINAL_0_Int Int) (hbv_ULTIMATE.start_ULTIMATE.startFINAL_1_Int Int) (hbv_ULTIMATE.start_ULTIMATE.startFINAL_2_Int Int) (hbv_ULTIMATE.start_ULTIMATE.startFINAL_3_Int Int) (hbv_ULTIMATE.start_ULTIMATE.startFINAL_4_Int Int) (hbv_ULTIMATE.start_ULTIMATE.startFINAL_5_Int Int) (hbv_ULTIMATE.start_ULTIMATE.startFINAL_6_Int Int) (hbv_ULTIMATE.start_ULTIMATE.startFINAL_7_Int Int) (hbv_ULTIMATE.start_ULTIMATE.startFINAL_8_Bool Bool)) (=> (ULTIMATE.start_ULTIMATE.startFINAL hhv_ULTIMATE.start_ULTIMATE.startEXIT_0_Int hhv_ULTIMATE.start_ULTIMATE.startEXIT_1_Int hhv_ULTIMATE.start_ULTIMATE.startEXIT_2_Int hhv_ULTIMATE.start_ULTIMATE.startEXIT_3_Int hhv_ULTIMATE.start_ULTIMATE.startEXIT_4_Int hhv_ULTIMATE.start_ULTIMATE.startEXIT_5_Int hhv_ULTIMATE.start_ULTIMATE.startEXIT_6_Int hhv_ULTIMATE.start_ULTIMATE.startEXIT_7_Int hhv_ULTIMATE.start_ULTIMATE.startEXIT_8_Bool) (ULTIMATE.start_ULTIMATE.startEXIT hhv_ULTIMATE.start_ULTIMATE.startEXIT_0_Int hhv_ULTIMATE.start_ULTIMATE.startEXIT_1_Int hhv_ULTIMATE.start_ULTIMATE.startEXIT_2_Int hhv_ULTIMATE.start_ULTIMATE.startEXIT_3_Int hhv_ULTIMATE.start_ULTIMATE.startEXIT_4_Int hhv_ULTIMATE.start_ULTIMATE.startEXIT_5_Int hhv_ULTIMATE.start_ULTIMATE.startEXIT_6_Int hhv_ULTIMATE.start_ULTIMATE.startEXIT_7_Int hhv_ULTIMATE.start_ULTIMATE.startEXIT_8_Bool))))
(assert (forall ((hhv_ULTIMATE.start_ULTIMATE.startENTRY_0_Int Int) (hhv_ULTIMATE.start_ULTIMATE.startENTRY_1_Int Int) (hhv_ULTIMATE.start_ULTIMATE.startENTRY_2_Int Int) (hhv_ULTIMATE.start_ULTIMATE.startENTRY_3_Int Int) (hhv_ULTIMATE.start_ULTIMATE.startENTRY_4_Int Int) (hhv_ULTIMATE.start_ULTIMATE.startENTRY_5_Int Int) (hhv_ULTIMATE.start_ULTIMATE.startENTRY_6_Int Int) (hhv_ULTIMATE.start_ULTIMATE.startENTRY_7_Int Int) (hhv_ULTIMATE.start_ULTIMATE.startENTRY_8_Bool Bool)) (=> (and (not hhv_ULTIMATE.start_ULTIMATE.startENTRY_8_Bool) (= hhv_ULTIMATE.start_ULTIMATE.startENTRY_0_Int hhv_ULTIMATE.start_ULTIMATE.startENTRY_1_Int)) (ULTIMATE.start_ULTIMATE.startENTRY hhv_ULTIMATE.start_ULTIMATE.startENTRY_0_Int hhv_ULTIMATE.start_ULTIMATE.startENTRY_1_Int hhv_ULTIMATE.start_ULTIMATE.startENTRY_2_Int hhv_ULTIMATE.start_ULTIMATE.startENTRY_3_Int hhv_ULTIMATE.start_ULTIMATE.startENTRY_4_Int hhv_ULTIMATE.start_ULTIMATE.startENTRY_5_Int hhv_ULTIMATE.start_ULTIMATE.startENTRY_6_Int hhv_ULTIMATE.start_ULTIMATE.startENTRY_7_Int hhv_ULTIMATE.start_ULTIMATE.startENTRY_8_Bool))))
(assert (forall ((hbv_ULTIMATE.start_ULTIMATE.startEXIT_0_Int Int) (hbv_ULTIMATE.start_ULTIMATE.startEXIT_1_Int Int) (hbv_ULTIMATE.start_ULTIMATE.startEXIT_2_Int Int) (hbv_ULTIMATE.start_ULTIMATE.startEXIT_3_Int Int) (hbv_ULTIMATE.start_ULTIMATE.startEXIT_4_Int Int) (hbv_ULTIMATE.start_ULTIMATE.startEXIT_5_Int Int) (hbv_ULTIMATE.start_ULTIMATE.startEXIT_6_Int Int) (hbv_ULTIMATE.start_ULTIMATE.startEXIT_7_Int Int) (hbv_ULTIMATE.start_ULTIMATE.startEXIT_8_Bool Bool)) (=> (and (ULTIMATE.start_ULTIMATE.startEXIT hbv_ULTIMATE.start_ULTIMATE.startEXIT_0_Int hbv_ULTIMATE.start_ULTIMATE.startEXIT_1_Int hbv_ULTIMATE.start_ULTIMATE.startEXIT_2_Int hbv_ULTIMATE.start_ULTIMATE.startEXIT_3_Int hbv_ULTIMATE.start_ULTIMATE.startEXIT_4_Int hbv_ULTIMATE.start_ULTIMATE.startEXIT_5_Int hbv_ULTIMATE.start_ULTIMATE.startEXIT_6_Int hbv_ULTIMATE.start_ULTIMATE.startEXIT_7_Int hbv_ULTIMATE.start_ULTIMATE.startEXIT_8_Bool) hbv_ULTIMATE.start_ULTIMATE.startEXIT_8_Bool) false)))
(check-sat)

smtinterpol d208e93

Exception in thread "main" java.lang.AssertionError
    at de.uni_freiburg.informatik.ultimate.smtinterpol.convert.SMTAffineTerm.<init>(SMTAffineTerm.java:83)
    at de.uni_freiburg.informatik.ultimate.smtinterpol.convert.Clausifier.addTermAxioms(Clausifier.java:1087)
    at de.uni_freiburg.informatik.ultimate.smtinterpol.convert.Clausifier$CCTermBuilder$BuildCCTerm.perform(Clausifier.java:128)
    at de.uni_freiburg.informatik.ultimate.smtinterpol.convert.Clausifier$CCTermBuilder.convert(Clausifier.java:181)
    at de.uni_freiburg.informatik.ultimate.smtinterpol.convert.Clausifier.addTermAxioms(Clausifier.java:1049)
    at de.uni_freiburg.informatik.ultimate.smtinterpol.convert.Clausifier.createEqualityProxy(Clausifier.java:1679)
    at de.uni_freiburg.informatik.ultimate.smtinterpol.theory.quant.SubstitutionHelper.substituteInClause(SubstitutionHelper.java:156)
    at de.uni_freiburg.informatik.ultimate.smtinterpol.theory.quant.InstantiationManager.computeClauseInstance(InstantiationManager.java:991)
    at de.uni_freiburg.informatik.ultimate.smtinterpol.theory.quant.InstantiationManager.instantiateSomeNotSat(InstantiationManager.java:283)
    at de.uni_freiburg.informatik.ultimate.smtinterpol.theory.quant.QuantifierTheory.computeConflictClause(QuantifierTheory.java:244)
    at de.uni_freiburg.informatik.ultimate.smtinterpol.dpll.DPLLEngine.checkConsistency(DPLLEngine.java:1010)
    at de.uni_freiburg.informatik.ultimate.smtinterpol.dpll.DPLLEngine.solve(DPLLEngine.java:1157)
    at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.SMTInterpol$CheckType$1.check(SMTInterpol.java:117)
    at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.SMTInterpol.checkSatAssuming(SMTInterpol.java:496)
    at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.SMTInterpol.checkSat(SMTInterpol.java:448)
    at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.Parser$Action$.CUP$do_action(Parser.java:2870)
    at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.Parser.do_action(Parser.java:1317)
    at com.github.jhoenicke.javacup.runtime.LRParser.parse(Unknown Source)
    at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.ParseEnvironment.parseStream(ParseEnvironment.java:119)
    at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.ParseEnvironment.parseScript(ParseEnvironment.java:98)
    at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.SMTLIB2Parser.run(SMTLIB2Parser.java:35)
    at de.uni_freiburg.informatik.ultimate.smtinterpol.Main.main(Main.java:165)
jhoenicke commented 5 months ago

Should be fixed now. Reports unknown though, because quantifier reasoning is incomplete.