search

uuverifiers / eldarica

The Eldarica model checker
Other
80 stars 22 forks source link

AssertionError at Predef.scala:156 (HornWrapper.scala:73) #22

Closed rainoftime closed 4 years ago

rainoftime commented 4 years ago

Hi , for the following instance,

(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)

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

Exception in thread "main" java.lang.AssertionError: assertion failed
        at scala.Predef$.assert(Predef.scala:156)
        at lazabs.horn.bottomup.HornWrapper$.verifySolution(HornWrapper.scala:73)
        at lazabs.horn.bottomup.InnerHornWrapper.<init>(HornWrapper.scala:380)
        at lazabs.horn.bottomup.HornWrapper$$anonfun$9.apply(HornWrapper.scala:228)
        at lazabs.horn.bottomup.HornWrapper$$anonfun$9.apply(HornWrapper.scala:230)
        at lazabs.ParallelComputation$.apply(ParallelComputation.scala:46)
        at lazabs.horn.bottomup.HornWrapper.<init>(HornWrapper.scala:227)
        at lazabs.horn.Solve$.apply(Solve.scala:81)
        at lazabs.Main$.doMain(Main.scala:586)
        at lazabs.Main$.main(Main.scala:267)
        at lazabs.Main.main(Main.scala)
pruemmer commented 4 years ago

This should also be fixed in 2.0.4.