uuverifiers / eldarica Goto Github PK

 Exception in thread "main" java.lang.AssertionError: assertion failed
        at scala.Predef$.assert(Predef.scala:156)
        at ap.basetypes.IdealInt.$up(IdealInt.scala:654)
        at ap.theories.bitvectors.ModReducer$Reducer$$anonfun$reduce$1$$anonfun$2.apply(ModReducer.scala:320)
        at ap.theories.bitvectors.ModReducer$Reducer$$anonfun$reduce$1$$anonfun$2.apply(ModReducer.scala:316)
        at ap.util.LRUCache.apply(LRUCache.scala:37)
        at ap.theories.bitvectors.ModReducer$Reducer$$anonfun$reduce$1.apply(ModReducer.scala:315)
        at ap.theories.bitvectors.ModReducer$Reducer$$anonfun$reduce$1.apply(ModReducer.scala:185)
        at ap.terfor.conjunctions.ReducerPlugin$.rewritePreds(ReducerPlugin.scala:89)
        at ap.theories.bitvectors.ModReducer$Reducer.reduce(ModReducer.scala:185)
        at ap.terfor.conjunctions.ReduceWithConjunction.ap$terfor$conjunctions$ReduceWithConjunction$$reduceWithPlugin(ReduceWithConjunction.scala:621)
        at ap.terfor.conjunctions.ReduceWithConjunction$.ap$terfor$conjunctions$ReduceWithConjunction$$reduceConj(ReduceWithConjunction.scala:91)
        at ap.terfor.conjunctions.ReduceWithConjunction$.ap$terfor$conjunctions$ReduceWithConjunction$$reduceConj(ReduceWithConjunction.scala:165)
        at ap.terfor.conjunctions.ReduceWithConjunction$$anonfun$1.apply(ReduceWithConjunction.scala:174)
        at ap.terfor.conjunctions.ReduceWithConjunction$$anonfun$1.apply(ReduceWithConjunction.scala:173)
        at scala.collection.TraversableLike$$anonfun$map$1.apply(TraversableLike.scala:234)
        at scala.collection.TraversableLike$$anonfun$map$1.apply(TraversableLike.scala:234)
        at scala.collection.Iterator$class.foreach(Iterator.scala:891)
        at scala.collection.AbstractIterator.foreach(Iterator.scala:1334)
        at scala.collection.IterableLike$class.foreach(IterableLike.scala:72)
        at ap.terfor.conjunctions.NegatedConjunctions.foreach(NegatedConjunctions.scala:72)
        at scala.collection.TraversableLike$class.map(TraversableLike.scala:234)
        at ap.terfor.conjunctions.NegatedConjunctions.map(NegatedConjunctions.scala:72)
        at ap.terfor.conjunctions.ReduceWithConjunction$.ap$terfor$conjunctions$ReduceWithConjunction$$reduceNegatedConjs(ReduceWithConjunction.scala:173)
...

'-assert', '-noSlicing', '-abstract:term'

$ java -jar Eldarica-assembly-2.0.3.jar -assert fname.smt2                              
Warning: ignoring exit
Theories: GroebnerMultiplication
Exception in thread "main" java.lang.AssertionError: assertion failed
        at scala.Predef$.assert(Predef.scala:156)
        at lazabs.horn.bottomup.HornWrapper$.verifyCEX(HornWrapper.scala:91)
        at lazabs.horn.bottomup.InnerHornWrapper.<init>(HornWrapper.scala:390)
        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:582)
        at lazabs.Main$.main(Main.scala:265)
        at lazabs.Main.main(Main.scala)

(set-logic HORN)
(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const i3 Int)
(assert (forall ((q11 Int) (q12 Bool)) (=> (not q12) (>= (* (* 88 88 (* 541 541 q11 q11 541) 541 q11) (- (* 145 318 (* 541 541 q11 q11 541) (* 541 541 q11 q11 541)) 318)) 541))))
(assert (forall ((q41 Int) (q42 Int) (q43 Int) (q44 Int) (q45 Int) (q46 Int) (q47 Bool)) (=> (<= 535 (+ 10 q42 q42 612 (- q43 (* 557 q43) (+ 564 q41 535 q45 q42) 936))) (not q47))))
(declare-const i5 Int)
(assert (forall ((q52 Int) (q53 Int) (q54 Int) (q55 Int) (q56 Int) (q57 Int) (q58 Int) (q59 Int) (q60 Int) (q61 Int) (q62 Int) (q63 Int) (q64 Bool)) (=> (distinct q60 q62) (or q64 q64 q64 q64 q64 q64 q64 q64))))
(assert (forall ((q80 Int) (q81 Int) (q82 Int) (q83 Bool)) (=> (distinct q83 q83 q83 q83 q83 q83 q83 q83) (= 162 450 (div (div q82 q82) 162)))))
(assert (forall ((q113 Int) (q114 Int) (q115 Int) (q116 Int) (q117 Int) (q118 Int) (q119 Int) (q120 Int) (q121 Int) (q122 Bool)) (=> (= q122 q122 q122) (<= q114 q113 680))))
(assert (forall ((q142 Int) (q143 Int) (q144 Int) (q145 Int) (q146 Int) (q147 Int) (q148 Int) (q149 Int) (q150 Int) (q151 Int) (q152 Bool)) (=> (= q152 q152 q152) (<= 894 19))))
(assert (forall ((q171 Int) (q172 Int) (q173 Int) (q174 Int) (q175 Int) (q176 Int) (q177 Int) (q178 Int) (q179 Int) (q180 Int) (q181 Int) (q182 Int) (q183 Bool)) (=> (not q183) (= q175 (mod q174 q177) q178 655))))
(assert (forall ((q184 Int) (q185 Int) (q186 Int) (q187 Int) (q188 Bool)) (=> (= q188 q188 q188 q188 q188 q188 q188) (<= (* 399 q186 (mod q185 q184) 114) q187 603))))
(assert (forall ((q189 Int) (q190 Int) (q191 Int) (q192 Int) (q193 Int) (q194 Int) (q195 Int) (q196 Int) (q197 Int) (q198 Int) (q199 Int) (q200 Int) (q201 Int) (q202 Int) (q203 Int) (q204 Int) (q205 Bool)) (=> (distinct q205 q205 q205 q205) (<= q201 q198))))
(assert (forall ((q206 Int) (q207 Int) (q208 Int) (q209 Int) (q210 Int) (q211 Int) (q212 Int) (q213 Int) (q214 Int) (q215 Int) (q216 Int) (q217 Int) (q218 Int) (q219 Int) (q220 Int) (q221 Bool)) (=> (< q210 (- q214)) (not q221))))
(assert (forall ((q222 Int) (q223 Int) (q224 Int) (q225 Int) (q226 Int) (q227 Int) (q228 Int) (q229 Int) (q230 Int) (q231 Int) (q232 Int) (q233 Int) (q234 Int) (q235 Int) (q236 Int) (q237 Int) (q238 Int) (q239 Int) (q240 Int) (q241 Bool)) (=> (=> q241 q241) (>= q237 (- 645) (- 645)))))
(assert (forall ((q242 Int) (q243 Int) (q244 Int) (q245 Int) (q246 Int) (q247 Int) (q248 Int) (q249 Int) (q250 Int) (q251 Bool)) (=> (>= 561 q249 q248) (=> q251 q251))))
(assert (forall ((q262 Int) (q263 Int) (q264 Int) (q265 Int) (q266 Int) (q267 Int) (q268 Int) (q269 Int) (q270 Int) (q271 Int) (q272 Int) (q273 Int) (q274 Int) (q275 Bool)) (=> (distinct q263 (mod (mod 398 84) 84) q269) (or q275 q275 q275 q275 q275 q275 q275))))
(declare-const i6 Int)
(assert (forall ((q289 Int) (q290 Int) (q291 Int) (q292 Int) (q293 Int) (q294 Int) (q295 Bool)) (=> (<= q293 q290 q290) (not q295))))
(assert (forall ((q304 Int) (q305 Int) (q306 Int) (q307 Bool)) (=> (> q306 507 q304) (not q307))))
(assert (forall ((q308 Int) (q309 Int) (q310 Int) (q311 Int) (q312 Int) (q313 Int) (q314 Int) (q315 Int) (q316 Bool)) (=> (> (+ q311 q308 q311 q310 q312) (+ q311 q308 q311 q310 q312) q310 (+ q311 159 159)) (=> q316 q316))))
(assert (forall ((q317 Int) (q318 Int) (q319 Int) (q320 Int) (q321 Int) (q322 Int) (q323 Int) (q324 Int) (q325 Int) (q326 Int) (q327 Int) (q328 Bool)) (=> (distinct q328 q328 q328 q328 q328 q328) (> q327 q319))))
(assert (forall ((q329 Int) (q330 Int) (q331 Int) (q332 Int) (q333 Bool)) (=> (=> q333 q333) (<= q331 233))))
(declare-const i7 Int)
(assert (forall ((q385 Int) (q386 Int) (q387 Int) (q388 Int) (q389 Int) (q390 Int) (q391 Int) (q392 Int) (q393 Int) (q394 Int) (q395 Int) (q396 Int) (q397 Int) (q398 Int) (q399 Int) (q400 Int) (q401 Int) (q402 Bool)) (=> (= q402 q402 q402 q402 q402 q402 q402) (= q401 q386))))
(assert (forall ((q404 Int) (q405 Int) (q406 Int) (q407 Int) (q408 Int) (q409 Int) (q410 Int) (q411 Int) (q412 Int) (q413 Int) (q414 Int) (q415 Int) (q416 Bool)) (=> (< 444 q413 q409) (and q416 q416 q416 q416 q416 q416 q416 q416 q416))))
(declare-const i8 Int)
(assert (forall ((q436 Int) (q437 Int) (q438 Int) (q439 Int) (q440 Int) (q441 Int) (q442 Int) (q443 Int) (q444 Int) (q445 Int) (q446 Int) (q447 Int) (q448 Int) (q449 Int) (q450 Bool)) (=> (or q450 q450 q450 q450 q450 q450) (> q440 q440 q441))))
(assert (forall ((q451 Int) (q452 Int) (q453 Int) (q454 Int) (q455 Int) (q456 Int) (q457 Int) (q458 Int) (q459 Int) (q460 Int) (q461 Int) (q462 Int) (q463 Int) (q464 Int) (q465 Int) (q466 Int) (q467 Int) (q468 Int) (q469 Int) (q470 Bool)) (=> (> q453 968 508) (or q470 q470 q470 q470 q470 q470 q470 q470))))
(declare-const i9 Int)
(assert (forall ((q485 Int) (q486 Int) (q487 Int) (q488 Int) (q489 Int) (q490 Int) (q491 Int) (q492 Int) (q493 Int) (q494 Int) (q495 Bool)) (=> (< q487 271 q489) (and q495 q495 q495 q495))))
(declare-const i10 Int) 
(assert (forall ((q535 Int) (q536 Int) (q537 Int) (q538 Int) (q539 Int) (q540 Int) (q541 Int) (q542 Int) (q543 Int) (q544 Int) (q545 Int) (q546 Int) (q547 Int) (q548 Int) (q549 Int) (q550 Int) (q551 Int) (q552 Bool)) (=> (> 549 (mod q550 (mod q536 q548))) (not q552))))
(assert (forall ((q553 Int) (q554 Int) (q555 Int) (q556 Int) (q557 Int) (q558 Int) (q559 Int) (q560 Int) (q561 Int) (q562 Int) (q563 Int) (q564 Int) (q565 Int) (q566 Int) (q567 Int) (q568 Int) (q569 Int) (q570 Int) (q571 Bool)) (=> (or q571 q571) (> q567 456 809 852))))
(assert (forall ((q572 Int) (q573 Int) (q574 Int) (q575 Int) (q576 Int) (q577 Int) (q578 Int) (q579 Int) (q580 Int) (q581 Int) (q582 Int) (q583 Bool)) (=> (= q583 q583 q583 q583 q583 q583 q583 q583 q583) (= 268 q580 248))))
(assert (forall ((q584 Int) (q585 Bool)) (=> (distinct q585 q585 q585 q585 q585 q585) (<= (* q584 900 806 q584) 900))))
(assert (forall ((q586 Int) (q587 Int) (q588 Int) (q589 Int) (q590 Int) (q591 Int) (q592 Int) (q593 Int) (q594 Bool)) (=> (distinct (div q586 46) 46 q586 q590) (not q594))))
(assert (forall ((q595 Int) (q596 Int) (q597 Int) (q598 Int) (q599 Bool)) (=> (distinct 660 989 q595 660) (= q599 q599 q599 q599 q599 q599 q599 q599 q599))))
(assert (forall ((q600 Int) (q601 Int) (q602 Int) (q603 Int) (q604 Int) (q605 Int) (q606 Int) (q607 Int) (q608 Int) (q609 Int) (q610 Int) (q611 Bool)) (=> (> q608 q600) (= q611 q611 q611 q611))))
(assert (forall ((q659 Int) (q660 Int) (q661 Int) (q662 Int) (q663 Int) (q664 Int) (q665 Int) (q666 Int) (q667 Int) (q668 Int) (q669 Int) (q670 Int) (q671 Int) (q672 Int) (q673 Int) (q674 Int) (q675 Int) (q676 Int) (q677 Int) (q678 Bool)) (=> (> q672 q669) (not q678))))
(declare-const i11 Int)
(assert (forall ((q682 Int) (q683 Int) (q684 Int) (q685 Int) (q686 Int) (q687 Int) (q688 Int) (q689 Int) (q690 Int) (q691 Int) (q692 Int) (q693 Bool)) (=> (< q692 306 q691 (- q687 (* q687 q690) (- q689 q686 306 306 q684))) (or q693 q693 q693 q693 q693 q693 q693 q693))))
(declare-const i12 Int)
(assert (forall ((q730 Int) (q731 Bool)) (=> (distinct q731 q731 q731 q731 q731 q731 q731 q731) (> (* q730 (* 449 215 449) 215 (* 449 215 449)) 984 (* (* 449 215 449) (+ 567 q730 567 (* 449 215 449)) 449) 449))))
(assert (forall ((q743 Int) (q744 Int) (q745 Int) (q746 Int) (q747 Int) (q748 Int) (q749 Int) (q750 Bool)) (=> (not q750) (> 623 358))))
(assert (forall ((q751 Int) (q752 Int) (q753 Int) (q754 Int) (q755 Int) (q756 Int) (q757 Int) (q758 Int) (q759 Bool)) (=> (>= q754 579 352) (= q759 q759 q759))))
(assert (forall ((q760 Int) (q761 Bool)) (=> (<= 793 q760 q760 793) (and q761 q761))))
(assert (forall ((q762 Int) (q763 Int) (q764 Int) (q765 Int) (q766 Int) (q767 Int) (q768 Int) (q769 Int) (q770 Int) (q771 Int) (q772 Int) (q773 Bool)) (=> (=> q773 q773) (<= q772 q769))))
(declare-const i13 Int)
(assert (forall ((q789 Int) (q790 Int) (q791 Int) (q792 Int) (q793 Int) (q794 Int) (q795 Int) (q796 Int) (q797 Int) (q798 Int) (q799 Bool)) (=> (not q799) (< 617 q796 q795))))
(assert (forall ((q800 Int) (q801 Int) (q802 Int) (q803 Int) (q804 Int) (q805 Int) (q806 Int) (q807 Int) (q808 Int) (q809 Int) (q810 Int) (q811 Int) (q812 Bool)) (=> (> q809 q803 q809 q809) (or q812 q812))))
(assert (forall ((q813 Int) (q814 Int) (q815 Int) (q816 Int) (q817 Int) (q818 Int) (q819 Int) (q820 Int) (q821 Int) (q822 Int) (q823 Bool)) (=> (distinct q823 q823) (>= q821 595))))
(declare-const i14 Int)
(assert (forall ((q824 Int) (q825 Int) (q826 Int) (q827 Int) (q828 Int) (q829 Int) (q830 Int) (q831 Int) (q832 Int) (q833 Int) (q834 Bool)) (=> (<= (abs q828) q827) (distinct q834 q834 q834 q834 q834 q834 q834 q834))))
(assert (forall ((q858 Int) (q859 Int) (q860 Int) (q861 Int) (q862 Bool)) (=> (= q861 q858 (* q861 (* q860 q860 (+ q860 q861) 781) 629 629)) (=> q862 q862))))
(assert (forall ((q863 Int) (q864 Int) (q865 Int) (q866 Int) (q867 Int) (q868 Int) (q869 Int) (q870 Int) (q871 Int) (q872 Int) (q873 Int) (q874 Int) (q875 Int) (q876 Int) (q877 Int) (q878 Int) (q879 Int) (q880 Int) (q881 Bool)) (=> (= q881 q881 q881 q881 q881 q881 q881 q881) (< q871 212 (+ q864 q869 q876 q874 842) (- q869 q872 q875 q865 q873)))))
(assert (forall ((q893 Int) (q894 Int) (q895 Int) (q896 Int) (q897 Bool)) (=> (and q897 q897 q897 q897 q897 q897) (<= (- q896 q894 q895) 916 (- q896 q894 q895)))))
(assert (forall ((q918 Int) (q919 Int) (q920 Int) (q921 Int) (q922 Int) (q923 Int) (q924 Int) (q925 Bool)) (=> (<= 291 (div (div 291 q918) q921)) (not q925))))
(assert (forall ((q944 Int) (q945 Int) (q946 Int) (q947 Int) (q948 Int) (q949 Int) (q950 Int) (q951 Int) (q952 Int) (q953 Int) (q954 Int) (q955 Int) (q956 Int) (q957 Int) (q958 Int) (q959 Int) (q960 Int) (q961 Bool)) (=> (<= q949 q946 q951) (=> q961 q961))))
(assert (forall ((q962 Int) (q963 Int) (q964 Int) (q965 Int) (q966 Bool)) (=> (>= q965 256) (not q966))))
(assert (forall ((q967 Int) (q968 Int) (q969 Bool)) (=> (= 456 q967) (=> q969 q969))))
(check-sat)

(set-logic HORN)
(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const bv_17-0 (_ BitVec 17))
(declare-const bv_29-0 (_ BitVec 29))
(assert (forall ((q0 (_ BitVec 10)) (q1 (_ BitVec 10)) (q2 (_ BitVec 10)) (q3 (_ BitVec 10)) (q4 (_ BitVec 10)) (q5 (_ BitVec 10)) (q6 (_ BitVec 10)) (q7 (_ BitVec 4))) (=> (bvsgt (bvsub q0 q5) q6) (bvuge q7 (bvsmod q7 (bvshl q7 q7))))))
(assert (forall ((q8 (_ BitVec 10)) (q9 (_ BitVec 10)) (q10 (_ BitVec 10)) (q11 (_ BitVec 10)) (q12 Bool)) (=> (distinct q12 q12 q12 q12 q12) (distinct (bvnor q10 q8) q10))))
(assert (forall ((q31 (_ BitVec 10)) (q32 (_ BitVec 10)) (q33 (_ BitVec 10)) (q34 (_ BitVec 10)) (q35 (_ BitVec 10)) (q36 (_ BitVec 10)) (q37 (_ BitVec 10)) (q38 (_ BitVec 10)) (q39 (_ BitVec 10)) (q40 (_ BitVec 10)) (q41 (_ BitVec 10)) (q42 (_ BitVec 10)) (q43 Bool)) (=> (xor q43 q43) (distinct (bvand q36 q37) (bvlshr q31 q37)))))
(assert (forall ((q44 (_ BitVec 10)) (q45 (_ BitVec 10)) (q46 (_ BitVec 10)) (q47 (_ BitVec 10)) (q48 (_ BitVec 10)) (q49 (_ BitVec 10)) (q50 (_ BitVec 10)) (q51 (_ BitVec 10)) (q52 (_ BitVec 10)) (q53 (_ BitVec 10)) (q54 (_ BitVec 10)) (q55 (_ BitVec 10)) (q56 (_ BitVec 10)) (q57 (_ BitVec 10)) (q58 (_ BitVec 10)) (q59 (_ BitVec 3))) (=> (bvsge q55 q53) (distinct q59 q59))))
(assert (forall ((q60 (_ BitVec 10)) (q61 (_ BitVec 10)) (q62 (_ BitVec 10)) (q63 (_ BitVec 10)) (q64 (_ BitVec 10)) (q65 (_ BitVec 10)) (q66 (_ BitVec 10)) (q67 (_ BitVec 10)) (q68 (_ BitVec 10)) (q69 (_ BitVec 10)) (q70 (_ BitVec 10)) (q71 (_ BitVec 10)) (q72 (_ BitVec 10)) (q73 (_ BitVec 10)) (q74 (_ BitVec 10)) (q75 (_ BitVec 4))) (=> (distinct (bvsrem q75 q75) q75) (distinct q63 (bvmul q68 q61)))))
(assert (forall ((q77 (_ BitVec 10)) (q78 (_ BitVec 10)) (q79 (_ BitVec 10)) (q80 (_ BitVec 10)) (q81 (_ BitVec 10)) (q82 (_ BitVec 10)) (q83 (_ BitVec 10)) (q84 (_ BitVec 10)) (q85 (_ BitVec 10)) (q86 (_ BitVec 10)) (q87 (_ BitVec 10)) (q88 (_ BitVec 10)) (q89 (_ BitVec 10)) (q90 (_ BitVec 10)) (q91 (_ BitVec 10)) (q92 (_ BitVec 10)) (q93 (_ BitVec 10)) (q94 (_ BitVec 10)) (q95 (_ BitVec 9))) (=> (= q87 q89) (distinct (bvnand q95 q95) (bvnand q95 q95)))))
(assert (forall ((q96 (_ BitVec 10)) (q97 (_ BitVec 10)) (q98 (_ BitVec 10)) (q99 (_ BitVec 10)) (q100 (_ BitVec 10)) (q101 (_ BitVec 10)) (q102 (_ BitVec 10)) (q103 (_ BitVec 10)) (q104 (_ BitVec 10)) (q105 (_ BitVec 10)) (q106 (_ BitVec 10)) (q107 (_ BitVec 10)) (q108 (_ BitVec 8))) (=> (= q104 q106) (= (bvor q108 q108) (bvor q108 q108)))))
(assert (forall ((q109 (_ BitVec 10)) (q110 (_ BitVec 10)) (q111 (_ BitVec 10)) (q112 (_ BitVec 10)) (q113 (_ BitVec 10)) (q114 (_ BitVec 10)) (q115 (_ BitVec 10)) (q116 (_ BitVec 10)) (q117 (_ BitVec 10)) (q118 (_ BitVec 10)) (q119 (_ BitVec 10)) (q120 (_ BitVec 10)) (q121 (_ BitVec 10)) (q122 (_ BitVec 10)) (q123 (_ BitVec 10)) (q124 (_ BitVec 10)) (q125 (_ BitVec 8))) (=> (bvult (bvnot q125) (bvnot q125)) (distinct q121 q114))))
(assert (forall ((q126 (_ BitVec 10)) (q127 (_ BitVec 10)) (q128 (_ BitVec 10)) (q129 (_ BitVec 10)) (q130 (_ BitVec 10)) (q131 (_ BitVec 10)) (q132 (_ BitVec 10)) (q133 (_ BitVec 10)) (q134 (_ BitVec 10)) (q135 (_ BitVec 10)) (q136 (_ BitVec 10)) (q137 (_ BitVec 10)) (q138 (_ BitVec 10)) (q139 (_ BitVec 4))) (=> (distinct q139 q139) (= q137 q131))))
(declare-const bv_4-1 (_ BitVec 4))
(assert (forall ((q140 (_ BitVec 10)) (q141 (_ BitVec 10)) (q142 (_ BitVec 10)) (q143 (_ BitVec 10)) (q144 (_ BitVec 10)) (q145 (_ BitVec 10)) (q146 (_ BitVec 10)) (q147 (_ BitVec 10)) (q148 (_ BitVec 10)) (q149 (_ BitVec 10)) (q150 (_ BitVec 10)) (q151 (_ BitVec 10)) (q152 (_ BitVec 10)) (q153 (_ BitVec 10)) (q154 (_ BitVec 10)) (q155 (_ BitVec 9))) (=> (distinct q155 q155) (= q151 (bvadd q140 q148)))))
(assert (forall ((q156 (_ BitVec 10)) (q157 (_ BitVec 10)) (q158 (_ BitVec 12))) (=> (= q158 ((_ sign_extend 0) q158)) (distinct q157 q157))))
(assert (forall ((q159 (_ BitVec 10)) (q160 (_ BitVec 10)) (q161 (_ BitVec 10)) (q162 (_ BitVec 10)) (q163 (_ BitVec 10)) (q164 (_ BitVec 10)) (q165 (_ BitVec 10)) (q166 (_ BitVec 10)) (q167 (_ BitVec 10)) (q168 (_ BitVec 10)) (q169 (_ BitVec 10)) (q170 (_ BitVec 10)) (q171 (_ BitVec 10)) (q172 (_ BitVec 10)) (q173 (_ BitVec 10)) (q174 (_ BitVec 10)) (q175 (_ BitVec 10)) (q176 (_ BitVec 10)) (q177 (_ BitVec 8))) (=> (= q164 q161) (bvsgt q177 (bvnor q177 q177)))))
(assert (forall ((q199 (_ BitVec 10)) (q200 (_ BitVec 10)) (q201 (_ BitVec 10)) (q202 (_ BitVec 10)) (q203 (_ BitVec 10)) (q204 (_ BitVec 10)) (q205 (_ BitVec 10)) (q206 (_ BitVec 10)) (q207 (_ BitVec 10)) (q208 (_ BitVec 10)) (q209 (_ BitVec 10)) (q210 (_ BitVec 10)) (q211 (_ BitVec 10)) (q212 (_ BitVec 10)) (q213 (_ BitVec 10)) (q214 (_ BitVec 10)) (q215 (_ BitVec 10)) (q216 (_ BitVec 10)) (q217 (_ BitVec 12))) (=> (distinct (bvsdiv q217 q217) (bvsmod q217 (bvsdiv q217 q217))) (= q209 q199))))
(assert (forall ((q225 (_ BitVec 10)) (q226 (_ BitVec 10)) (q227 (_ BitVec 10)) (q228 (_ BitVec 10)) (q229 (_ BitVec 10)) (q230 (_ BitVec 10)) (q231 (_ BitVec 10)) (q232 (_ BitVec 10)) (q233 (_ BitVec 10)) (q234 (_ BitVec 10)) (q235 (_ BitVec 10)) (q236 (_ BitVec 10)) (q237 (_ BitVec 16))) (=> (distinct q237 q237) (bvult q233 q231))))
(declare-const bv_4-2 (_ BitVec 4))
(assert (forall ((q238 (_ BitVec 10)) (q239 (_ BitVec 10)) (q240 (_ BitVec 10)) (q241 (_ BitVec 10)) (q242 (_ BitVec 10)) (q243 (_ BitVec 10)) (q244 (_ BitVec 10)) (q245 (_ BitVec 10)) (q246 (_ BitVec 10)) (q247 (_ BitVec 10)) (q248 (_ BitVec 10)) (q249 (_ BitVec 10)) (q250 (_ BitVec 10)) (q251 (_ BitVec 10)) (q252 (_ BitVec 10)) (q253 (_ BitVec 10)) (q254 (_ BitVec 10)) (q255 (_ BitVec 29))) (=> (bvslt (bvsmod q255 q255) q255) (= q249 q248))))
(assert (forall ((q256 (_ BitVec 10)) (q257 (_ BitVec 10)) (q258 (_ BitVec 10)) (q259 (_ BitVec 10)) (q260 (_ BitVec 10)) (q261 (_ BitVec 10)) (q262 (_ BitVec 4))) (=> (bvugt q257 q259) (= (bvashr q262 q262) q262))))
(assert (forall ((q263 (_ BitVec 10)) (q264 (_ BitVec 10)) (q265 (_ BitVec 10)) (q266 (_ BitVec 10)) (q267 (_ BitVec 10)) (q268 (_ BitVec 10)) (q269 (_ BitVec 9))) (=> (bvsgt (bvadd q269 q269) (bvadd q269 q269)) (= q268 q268))))
(assert (forall ((q270 (_ BitVec 10)) (q271 (_ BitVec 10)) (q272 (_ BitVec 10)) (q273 (_ BitVec 10)) (q274 (_ BitVec 10)) (q275 (_ BitVec 10)) (q276 (_ BitVec 10)) (q277 (_ BitVec 10)) (q278 (_ BitVec 10)) (q279 (_ BitVec 10)) (q280 (_ BitVec 4))) (=> (distinct q279 q276) (= (bvor q280 q280) q280))))
(assert (forall ((q287 (_ BitVec 10)) (q288 (_ BitVec 10)) (q289 (_ BitVec 10)) (q290 (_ BitVec 10)) (q291 (_ BitVec 10)) (q292 (_ BitVec 10)) (q293 (_ BitVec 10)) (q294 (_ BitVec 10)) (q295 (_ BitVec 10)) (q296 (_ BitVec 10)) (q297 (_ BitVec 10)) (q298 (_ BitVec 10)) (q299 (_ BitVec 10)) (q300 (_ BitVec 10)) (q301 (_ BitVec 10)) (q302 (_ BitVec 10)) (q303 (_ BitVec 10)) (q304 (_ BitVec 10)) (q305 (_ BitVec 10)) (q306 (_ BitVec 10)) (q307 (_ BitVec 9))) (=> (= (bvnot q307) q307) (distinct q304 q304))))
(assert (forall ((q308 (_ BitVec 10)) (q309 (_ BitVec 10)) (q310 (_ BitVec 10)) (q311 (_ BitVec 10)) (q312 (_ BitVec 10)) (q313 (_ BitVec 10)) (q314 (_ BitVec 17))) (=> (bvslt q312 q312) (distinct (bvneg q314) (bvnot q314)))))
(assert (forall ((q315 (_ BitVec 10)) (q316 (_ BitVec 10)) (q317 (_ BitVec 10)) (q318 (_ BitVec 10)) (q319 (_ BitVec 10)) (q320 (_ BitVec 10)) (q321 (_ BitVec 10)) (q322 (_ BitVec 10)) (q323 (_ BitVec 10)) (q324 (_ BitVec 10)) (q325 (_ BitVec 10)) (q326 (_ BitVec 10)) (q327 (_ BitVec 10)) (q328 (_ BitVec 29))) (=> (distinct (bvmul q328 q328) (bvmul q328 q328)) (distinct (bvsmod q318 q326) q315))))
(assert (forall ((q329 (_ BitVec 10)) (q330 (_ BitVec 10)) (q331 (_ BitVec 10)) (q332 (_ BitVec 10)) (q333 (_ BitVec 10)) (q334 (_ BitVec 10)) (q335 (_ BitVec 10)) (q336 (_ BitVec 10)) (q337 (_ BitVec 10)) (q338 (_ BitVec 10)) (q339 (_ BitVec 10)) (q340 (_ BitVec 10)) (q341 (_ BitVec 9))) (=> (bvult (bvurem q341 q341) (bvsmod q341 q341)) (bvsgt q333 q334))))
(declare-const bv_9-1 (_ BitVec 9))
(assert (forall ((q342 (_ BitVec 10)) (q343 (_ BitVec 10)) (q344 (_ BitVec 10)) (q345 (_ BitVec 10)) (q346 (_ BitVec 10)) (q347 (_ BitVec 10)) (q348 (_ BitVec 10)) (q349 (_ BitVec 10)) (q350 (_ BitVec 10)) (q351 (_ BitVec 10)) (q352 (_ BitVec 10)) (q353 (_ BitVec 10)) (q354 (_ BitVec 10)) (q355 (_ BitVec 10)) (q356 (_ BitVec 10)) (q357 (_ BitVec 10)) (q358 (_ BitVec 10)) (q359 (_ BitVec 16))) (=> (distinct q345 q354) (= (bvsub q359 q359) (bvsub q359 q359)))))
(assert (forall ((q360 (_ BitVec 10)) (q361 (_ BitVec 10)) (q362 (_ BitVec 10)) (q363 (_ BitVec 10)) (q364 (_ BitVec 10)) (q365 (_ BitVec 10)) (q366 (_ BitVec 16))) (=> (= q366 q366) (= q360 q365))))
(declare-const bv_2-0 (_ BitVec 2))
(assert (forall ((q367 (_ BitVec 10)) (q368 (_ BitVec 10)) (q369 (_ BitVec 10)) (q370 (_ BitVec 10)) (q371 (_ BitVec 10)) (q372 (_ BitVec 10)) (q373 (_ BitVec 10)) (q374 (_ BitVec 10)) (q375 (_ BitVec 10)) (q376 (_ BitVec 10)) (q377 (_ BitVec 10)) (q378 (_ BitVec 3))) (=> (bvsge q376 q376) (distinct (bvand q378 q378) (bvand (bvand q378 q378) q378)))))
(assert (forall ((q379 (_ BitVec 10)) (q380 (_ BitVec 10)) (q381 (_ BitVec 10)) (q382 (_ BitVec 10)) (q383 (_ BitVec 10)) (q384 (_ BitVec 10)) (q385 (_ BitVec 10)) (q386 (_ BitVec 10)) (q387 (_ BitVec 10)) (q388 (_ BitVec 10)) (q389 (_ BitVec 10)) (q390 (_ BitVec 10)) (q391 (_ BitVec 10)) (q392 (_ BitVec 10)) (q393 (_ BitVec 9))) (=> (distinct (bvsub q382 q387) q383) (distinct (bvsub q393 q393) (bvadd q393 (bvsub q393 q393))))))
(assert (forall ((q394 (_ BitVec 10)) (q395 (_ BitVec 2))) (=> (= q395 q395) (= q394 q394))))
(declare-const bv_13-0 (_ BitVec 13))
(declare-const bv_8-4 (_ BitVec 8))
(assert (forall ((q398 (_ BitVec 10)) (q399 (_ BitVec 10)) (q400 (_ BitVec 10)) (q401 (_ BitVec 10)) (q402 (_ BitVec 10)) (q403 (_ BitVec 13))) (=> (distinct q402 q400) (= (bvnot (bvlshr q403 q403)) (bvashr (bvnand q403 q403) (bvnand q403 q403))))))
(assert (forall ((q404 (_ BitVec 10)) (q405 (_ BitVec 9))) (=> (bvsge q405 q405) (= q404 (bvudiv q404 q404)))))
(assert (forall ((q406 (_ BitVec 10)) (q407 (_ BitVec 10)) (q408 (_ BitVec 10)) (q409 (_ BitVec 4))) (=> (= q409 q409) (distinct q408 (bvand q406 q407)))))
(assert (forall ((q410 (_ BitVec 10)) (q411 (_ BitVec 10)) (q412 (_ BitVec 10)) (q413 (_ BitVec 10)) (q414 (_ BitVec 10)) (q415 (_ BitVec 10)) (q416 (_ BitVec 10)) (q417 (_ BitVec 10)) (q418 (_ BitVec 10)) (q419 (_ BitVec 10)) (q420 (_ BitVec 10)) (q421 (_ BitVec 10)) (q422 (_ BitVec 10)) (q423 (_ BitVec 10)) (q424 (_ BitVec 10)) (q425 (_ BitVec 10)) (q426 (_ BitVec 10)) (q427 (_ BitVec 10)) (q428 (_ BitVec 29))) (=> (distinct q415 q427) (= (bvurem q428 q428) q428))))
(assert (forall ((q429 (_ BitVec 10)) (q430 (_ BitVec 10)) (q431 (_ BitVec 10)) (q432 (_ BitVec 10)) (q433 (_ BitVec 10)) (q434 (_ BitVec 10)) (q435 (_ BitVec 10)) (q436 (_ BitVec 10)) (q437 (_ BitVec 10)) (q438 (_ BitVec 10)) (q439 (_ BitVec 10)) (q440 (_ BitVec 10)) (q441 (_ BitVec 10)) (q442 Bool)) (=> (= q437 q434) (or q442 q442 q442 q442 q442))))
(assert (forall ((q443 (_ BitVec 10)) (q444 (_ BitVec 10)) (q445 (_ BitVec 10)) (q446 (_ BitVec 10)) (q447 (_ BitVec 10)) (q448 (_ BitVec 10)) (q449 (_ BitVec 10)) (q450 (_ BitVec 10)) (q451 (_ BitVec 10)) (q452 (_ BitVec 10)) (q453 (_ BitVec 10)) (q454 (_ BitVec 10)) (q455 (_ BitVec 10)) (q456 (_ BitVec 10)) (q457 (_ BitVec 10)) (q458 (_ BitVec 10)) (q459 (_ BitVec 10)) (q460 (_ BitVec 10)) (q461 (_ BitVec 10)) (q462 (_ BitVec 10)) (q463 (_ BitVec 10)) (q464 (_ BitVec 13))) (=> (= q443 q450) (= q464 q464))))
(assert (forall ((q465 (_ BitVec 10)) (q466 (_ BitVec 10)) (q467 (_ BitVec 10)) (q468 (_ BitVec 10)) (q469 (_ BitVec 10)) (q470 (_ BitVec 10)) (q471 (_ BitVec 10)) (q472 (_ BitVec 10)) (q473 (_ BitVec 10)) (q474 (_ BitVec 10)) (q475 (_ BitVec 10)) (q476 (_ BitVec 10)) (q477 (_ BitVec 10)) (q478 (_ BitVec 10)) (q479 Bool)) (=> (and q479 q479 q479 q479 q479 q479 q479) (distinct (bvmul q477 q467) q478))))
(assert (forall ((q480 (_ BitVec 10)) (q481 (_ BitVec 10)) (q482 (_ BitVec 10)) (q483 (_ BitVec 10)) (q484 (_ BitVec 10)) (q485 (_ BitVec 10)) (q486 (_ BitVec 10)) (q487 (_ BitVec 10)) (q488 (_ BitVec 10)) (q489 (_ BitVec 10)) (q490 (_ BitVec 10)) (q491 (_ BitVec 10)) (q492 (_ BitVec 10)) (q493 (_ BitVec 10)) (q494 (_ BitVec 10)) (q495 (_ BitVec 10)) (q496 (_ BitVec 29))) (=> (bvuge (bvand (bvsrem q496 q496) q496) (bvand (bvsrem q496 q496) q496)) (= q493 q483))))
(declare-const bv_2-1 (_ BitVec 2))
(assert (forall ((q518 (_ BitVec 10)) (q519 (_ BitVec 10)) (q520 (_ BitVec 10)) (q521 (_ BitVec 10)) (q522 (_ BitVec 10)) (q523 (_ BitVec 10)) (q524 (_ BitVec 10)) (q525 (_ BitVec 10)) (q526 (_ BitVec 10)) (q527 (_ BitVec 10)) (q528 (_ BitVec 10)) (q529 (_ BitVec 10)) (q530 (_ BitVec 10)) (q531 (_ BitVec 10)) (q532 (_ BitVec 10)) (q533 (_ BitVec 10)) (q534 (_ BitVec 10)) (q535 (_ BitVec 10)) (q536 (_ BitVec 10)) (q537 (_ BitVec 13))) (=> (bvule q521 (bvsmod q535 q524)) (distinct (bvsmod (bvshl q537 q537) (bvsrem q537 q537)) q537))))
(assert (forall ((q538 (_ BitVec 10)) (q539 (_ BitVec 10)) (q540 (_ BitVec 16))) (=> (distinct (bvor q538 q539) (bvor q538 q539)) (bvult (bvsmod q540 q540) q540))))
(assert (forall ((q541 (_ BitVec 10)) (q542 (_ BitVec 10)) (q543 (_ BitVec 10)) (q544 (_ BitVec 10)) (q545 (_ BitVec 10)) (q546 (_ BitVec 10)) (q547 (_ BitVec 10)) (q548 (_ BitVec 10)) (q549 (_ BitVec 10)) (q550 (_ BitVec 10)) (q551 (_ BitVec 10)) (q552 (_ BitVec 10)) (q553 (_ BitVec 10)) (q554 (_ BitVec 10)) (q555 (_ BitVec 10)) (q556 (_ BitVec 8))) (=> (bvslt q556 q556) (distinct q544 q552))))
(assert (forall ((q557 (_ BitVec 10)) (q558 (_ BitVec 10)) (q559 (_ BitVec 10)) (q560 (_ BitVec 10)) (q561 (_ BitVec 10)) (q562 (_ BitVec 10)) (q563 (_ BitVec 10)) (q564 (_ BitVec 10)) (q565 (_ BitVec 10)) (q566 (_ BitVec 10)) (q567 (_ BitVec 10)) (q568 (_ BitVec 10)) (q569 (_ BitVec 16))) (=> (= q564 q557) (= (bvshl q569 q569) (bvadd (bvshl q569 q569) (bvmul q569 (bvshl q569 q569)))))))
(assert (forall ((q570 (_ BitVec 10)) (q571 (_ BitVec 10)) (q572 (_ BitVec 10)) (q573 (_ BitVec 10)) (q574 (_ BitVec 10)) (q575 (_ BitVec 10)) (q576 (_ BitVec 10)) (q577 (_ BitVec 10)) (q578 (_ BitVec 10)) (q579 (_ BitVec 10)) (q580 (_ BitVec 10)) (q581 Bool)) (=> (bvsle q571 q580) (= q581 q581))))
(assert (forall ((q582 (_ BitVec 10)) (q583 (_ BitVec 10)) (q584 (_ BitVec 10)) (q585 (_ BitVec 10)) (q586 (_ BitVec 10)) (q587 (_ BitVec 9))) (=> (distinct (bvlshr q587 (bvlshr q587 q587)) (bvlshr q587 (bvlshr q587 q587))) (distinct q583 q586))))
(assert (forall ((q588 (_ BitVec 10)) (q589 (_ BitVec 10)) (q590 (_ BitVec 10)) (q591 (_ BitVec 10)) (q592 (_ BitVec 10)) (q593 (_ BitVec 10)) (q594 (_ BitVec 10)) (q595 (_ BitVec 10)) (q596 (_ BitVec 10)) (q597 (_ BitVec 10)) (q598 (_ BitVec 10)) (q599 (_ BitVec 10)) (q600 (_ BitVec 10)) (q601 (_ BitVec 10)) (q602 (_ BitVec 29))) (=> (distinct q602 q602) (distinct q600 q597))))
(assert (forall ((q603 (_ BitVec 10)) (q604 (_ BitVec 10)) (q605 (_ BitVec 10)) (q606 (_ BitVec 10)) (q607 (_ BitVec 10)) (q608 (_ BitVec 10)) (q609 (_ BitVec 10)) (q610 (_ BitVec 10)) (q611 (_ BitVec 10)) (q612 (_ BitVec 10)) (q613 (_ BitVec 10)) (q614 (_ BitVec 10)) (q615 (_ BitVec 10)) (q616 (_ BitVec 29))) (=> (= q616 q616) (distinct (bvand q612 q607) q612))))
(declare-const bv_18-0 (_ BitVec 18))
(assert (forall ((q617 (_ BitVec 10)) (q618 (_ BitVec 10)) (q619 (_ BitVec 10)) (q620 (_ BitVec 11))) (=> (distinct q620 q620) (bvugt (bvudiv q619 q617) (bvudiv q619 q617)))))
(assert (forall ((q644 (_ BitVec 10)) (q645 (_ BitVec 10)) (q646 (_ BitVec 10)) (q647 (_ BitVec 10)) (q648 (_ BitVec 10)) (q649 (_ BitVec 10)) (q650 (_ BitVec 10)) (q651 (_ BitVec 10)) (q652 (_ BitVec 10)) (q653 (_ BitVec 10)) (q654 (_ BitVec 10)) (q655 (_ BitVec 10)) (q656 (_ BitVec 10)) (q657 (_ BitVec 10)) (q658 (_ BitVec 10)) (q659 (_ BitVec 10)) (q660 (_ BitVec 10)) (q661 (_ BitVec 11))) (=> (distinct q651 q660) (bvult (bvshl q661 q661) (bvsrem q661 (bvshl q661 q661))))))
(assert (forall ((q662 (_ BitVec 10)) (q663 (_ BitVec 10)) (q664 (_ BitVec 10)) (q665 (_ BitVec 8))) (=> (distinct q662 q663) (= (bvshl q665 (bvadd q665 q665)) q665))))
(declare-const bv_15-0 (_ BitVec 15))
(assert (forall ((q666 (_ BitVec 10)) (q667 (_ BitVec 10)) (q668 (_ BitVec 10)) (q669 (_ BitVec 10)) (q670 (_ BitVec 10)) (q671 (_ BitVec 10)) (q672 (_ BitVec 10)) (q673 (_ BitVec 16))) (=> (bvult q668 q672) (= q673 (bvsdiv q673 (bvsub q673 q673))))))
(assert (forall ((q674 (_ BitVec 10)) (q675 (_ BitVec 10)) (q676 (_ BitVec 10)) (q677 (_ BitVec 10)) (q678 (_ BitVec 29))) (=> (bvult q678 (bvneg q678)) (bvule q676 q674))))
(check-sat)

 Theories: GroebnerMultiplication, ModuloArithmetic
 Exception in thread "main" java.lang.AssertionError: assertion failed
        at scala.Predef$.assert(Predef.scala:156)
        at ap.util.Debug$.assertTrue(Debug.scala:111)
        at ap.util.Debug$.assertInt(Debug.scala:144)
        at ap.theories.bitvectors.LShiftCastSplitter$$anonfun$shiftCastActions$3.apply(ShiftCastSplitter.scala:152)
        at ap.theories.bitvectors.LShiftCastSplitter$$anonfun$shiftCastActions$3.apply(ShiftCastSplitter.scala:75)
        at scala.collection.mutable.ResizableArray$class.foreach(ResizableArray.scala:59)
        at scala.collection.mutable.ArrayBuffer.foreach(ArrayBuffer.scala:48)
        at ap.theories.bitvectors.LShiftCastSplitter$.shiftCastActions(ShiftCastSplitter.scala:75)
        at ap.theories.bitvectors.ModPlugin$.modShiftCast(ModPlugin.scala:209)
        at ap.theories.bitvectors.ModPlugin$.handleGoal(ModPlugin.scala:166)
        at ap.proof.theoryPlugins.PluginSequence.handleGoal(Plugin.scala:238)                                                                                                                    
        at ap.proof.theoryPlugins.PluginTask.apply(Plugin.scala:392)
        at ap.proof.goal.Goal.step(Goal.scala:395)
        at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:470)
        at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:476)
        at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:476)
        at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:589)
        at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:476)
        at ap.proof.ModelSearchProver$IncProverImpl.checkValidityDir(ModelSearchProver.scala:1079)
        at ap.proof.ModelSearchProver$IncProverImpl.checkValidityDir(ModelSearchProver.scala:1069)
        at ap.proof.ModelSearchProver$IncProverImpl.checkValidity(ModelSearchProver.scala:1057)
        at lazabs.horn.bottomup.HornPredAbs$$anonfun$isValid$1.apply$mcZ$sp(HornPredAbs.scala:703)
        at lazabs.horn.bottomup.HornPredAbs$$anonfun$isValid$1.apply(HornPredAbs.scala:694)
。。

(set-logic HORN)
(declare-fun
   INV_MAIN_0
   (Int
    Int)
   Bool)
(assert
 (forall
  ((HEAP$1 (Array Int Int))
   (i1 Int))
  (INV_MAIN_0 i1 (select HEAP$1 i1))))
(assert
 (forall
  ((i1 Int)
   (heap1 Int))
  (=>
   (INV_MAIN_0 i1 heap1)
   true)))
(check-sat)
(get-model)

(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 i0 Int)
(assert (forall ((q0 Int) (q1 Bool)) (=> (= (mod 998 q0) (mod 998 (mod q0 q0)) (mod q0 q0)) (or q1 q1))))
(declare-const i5 Int)
(assert (forall ((q7 Int) (q8 Bool)) (=> (not q8) (distinct 734 (+ (* q7 (+ 378 (abs 974) 607 378 705) 607) q7 856) 995 (+ 378 (abs 974) 607 378 705)))))
(assert (forall ((q9 Int) (q10 Int) (q11 Bool)) (=> (=> q11 q11) (<= (- q10 q9 q9) (* (* 1 183 q10) 126) (div (* (* 1 183 q10) 126) q9)))))
(assert (forall ((q12 Int) (q13 Int) (q14 Int) (q15 Bool)) (=> (= 258 60 (mod q12 886)) (or q15 q15 q15 q15))))
(assert (forall ((q19 Int) (q20 Int) (q21 Int) (q22 Bool)) (=> (not q22) (< 187 (- q21)))))
(declare-const i6 Int)
(assert (forall ((q41 Int) (q42 Int) (q43 Int) (q44 Bool)) (=> (and q44 q44 q44 q44 q44 q44 q44 q44 q44) (>= (mod 483 90) 543 483))))
(assert (forall ((q48 Int) (q49 Int) (q50 Bool)) (=> (> q49 108 849) (=> q50 q50))))
(declare-const i7 Int)
(assert (forall ((q57 Int) (q58 Int) (q59 Int) (q60 Bool)) (=> (or q60 q60 q60 q60 q60 q60 q60 q60 q60) (<= (div q58 q58) 740 (div q58 q58)))))
(declare-const i8 Int)
(assert (forall ((q70 Int) (q71 Int) (q72 Bool)) (=> (> 53 q71 273 q71) (and q72 q72 q72 q72 q72 q72 q72 q72 q72))))
(assert (forall ((q73 Int) (q74 Bool)) (=> (<= (- 513) q73) (and q74 q74 q74 q74 q74 q74))))
(assert (forall ((q79 Int) (q80 Int) (q81 Bool)) (=> (= q80 553) (=> q81 q81))))
(assert (forall ((q87 Int) (q88 Bool)) (=> (<= (- (+ 50 q87) (+ 50 q87) 323 (- q87 323 q87)) (+ (- (+ 50 q87) (+ 50 q87) 323 (- q87 323 q87)) 50 (- q87 323 q87) q87) (- q87 323 q87) (+ (- (+ 50 q87) (+ 50 q87) 323 (- q87 323 q87)) 50 (- q87 323 q87) q87)) (= q88 q88 q88 q88 q88 q88))))
(assert (forall ((q104 Int) (q105 Bool)) (=> (distinct q105 q105 q105 q105 q105) (> 520 520 (mod 800 (mod (div q104 756) 756))))))
(assert (forall ((q109 Int) (q110 Bool)) (=> (distinct 551 (div (mod (mod q109 73) 73) 370)) (= q110 q110 q110 q110 q110 q110))))
(assert (forall ((q122 Int) (q123 Int) (q124 Bool)) (=> (> q123 q123) (or q124 q124 q124 q124))))
(check-sat)

-assert -noSlicing -abstract:relEqs

Theories: GroebnerMultiplication
 Exception in thread "main" java.lang.AssertionError: assertion failed
        at scala.Predef$.assert(Predef.scala:156)
        at ap.theories.nia.Polynomial.<init>(Polynomial.scala:580)
        at ap.theories.nia.Polynomial.$div(Polynomial.scala:655)
        at ap.theories.nia.GroebnerMultiplication$$anon$1$$anonfun$ap$theories$nia$GroebnerMultiplication$$anon$$handleGoalAux$3.apply(GroebnerMultiplication.scala:490)
        at ap.theories.nia.GroebnerMultiplication$$anon$1$$anonfun$ap$theories$nia$GroebnerMultiplication$$anon$$handleGoalAux$3.apply(GroebnerMultiplication.scala:483)
        at scala.collection.IndexedSeqOptimized$class.foreach(IndexedSeqOptimized.scala:33)
        at scala.collection.mutable.ArrayOps$ofRef.foreach(ArrayOps.scala:186)
        at ap.theories.nia.GroebnerMultiplication$$anon$1.ap$theories$nia$GroebnerMultiplication$$anon$$handleGoalAux(GroebnerMultiplication.scala:483)
        at ap.theories.nia.GroebnerMultiplication$$anon$1.handleGoal(GroebnerMultiplication.scala:212)
        at ap.proof.theoryPlugins.PluginTask.apply(Plugin.scala:392)
        at ap.proof.goal.Goal.step(Goal.scala:395)
        at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:470)
        at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:589)
        at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:476)
        at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:589)
        at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:476)
        at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:589)
        at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:476)
        at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:589)
        at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:476)
        at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:476)
        at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:476)
        at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:589)
        at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:476)
        at ap.proof.ModelSearchProver$IncProverImpl.checkValidityDir(ModelSearchProver.scala:1079)
        at ap.proof.ModelSearchProver$IncProverImpl.checkValidityDir(ModelSearchProver.scala:1069)
        at ap.proof.ModelSearchProver$IncProverImpl.checkValidity(ModelSearchProver.scala:1057)
        at lazabs.horn.bottomup.HornPredAbs$$anonfun$isValid$1.apply$mcZ$sp(HornPredAbs.scala:703)
        at lazabs.horn.bottomup.HornPredAbs$$anonfun$isValid$1.apply(HornPredAbs.scala:694)
        at lazabs.horn.bottomup.HornPredAbs$$anonfun$isValid$1.apply(HornPredAbs.scala:694)
        at scala.util.DynamicVariable.withValue(DynamicVariable.scala:58)
        at ap.util.Timeout$.withChecker(Timeout.scala:44)
        at lazabs.horn.bottomup.HornPredAbs.isValid(HornPredAbs.scala:694)
        at lazabs.horn.bottomup.HornPredAbs$$anonfun$genEdge$1.apply(HornPredAbs.scala:1457)
        at lazabs.horn.bottomup.HornPredAbs$$anonfun$genEdge$1.apply(HornPredAbs.scala:1448)
        at lazabs.horn.bottomup.Hasher.scope(Hasher.scala:356)
        at lazabs.horn.bottomup.HornPredAbs.genEdge(HornPredAbs.scala:1448)
        at lazabs.horn.bottomup.Hasher.scope(Hasher.scala:356)
        at lazabs.horn.bottomup.HornPredAbs.genEdge(HornPredAbs.scala:1448)
        at lazabs.horn.bottomup.HornPredAbs.liftedTree1$1(HornPredAbs.scala:870)
        at lazabs.horn.bottomup.HornPredAbs.<init>(HornPredAbs.scala:869)
        at lazabs.horn.bottomup.InnerHornWrapper$$anonfun$26.apply(HornWrapper.scala:398)
        at lazabs.horn.bottomup.InnerHornWrapper$$anonfun$26.apply(HornWrapper.scala:392)
        at scala.util.DynamicVariable.withValue(DynamicVariable.scala:58)
        at scala.Console$.withOut(Console.scala:65)
        at lazabs.horn.bottomup.InnerHornWrapper.<init>(HornWrapper.scala:392)
        at lazabs.horn.bottomup.HornWrapper$$anonfun$11.apply(HornWrapper.scala:254)
        at lazabs.horn.bottomup.HornWrapper$$anonfun$11.apply(HornWrapper.scala:256)
        at lazabs.ParallelComputation$.apply(ParallelComputation.scala:46)
        at lazabs.horn.bottomup.HornWrapper.<init>(HornWrapper.scala:253)
        at lazabs.horn.Solve$.apply(Solve.scala:81)
        at lazabs.Main$.doMain(Main.scala:601)
        at lazabs.Main$.main(Main.scala:271)
        at lazabs.Main.main(Main.scala)

(set-logic HORN)
(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const bv_3-0 (_ BitVec 3))
(assert (forall ((q0 (_ BitVec 7)) (q1 (_ BitVec 7)) (q2 (_ BitVec 7)) (q3 (_ BitVec 7)) (q4 (_ BitVec 7)) (q5 (_ BitVec 10))) (=> (distinct q2 q2) (bvslt (bvor q5 q5) (bvor q5 q5)))))
(assert (forall ((q6 (_ BitVec 7)) (q7 (_ BitVec 7)) (q8 (_ BitVec 7)) (q9 (_ BitVec 7)) (q10 (_ BitVec 10))) (=> (bvslt (bvsmod q10 (bvlshr q10 q10)) (bvlshr q10 q10)) (distinct (bvnot q8) (bvnot q8)))))
(assert (forall ((q11 (_ BitVec 7)) (q12 (_ BitVec 7)) (q13 (_ BitVec 7)) (q14 (_ BitVec 7)) (q15 (_ BitVec 7)) (q16 (_ BitVec 7)) (q17 (_ BitVec 7)) (q18 (_ BitVec 7)) (q19 (_ BitVec 7)) (q20 (_ BitVec 7
)) (q21 (_ BitVec 7)) (q22 (_ BitVec 7)) (q23 (_ BitVec 7)) (q24 (_ BitVec 10))) (=> (= q22 (bvnot (bvadd q22 q20))) (= (bvlshr q24 q24) (bvlshr q24 q24)))))
(declare-const bv_8-0 (_ BitVec 8))
(assert (forall ((q25 (_ BitVec 7)) (q26 (_ BitVec 7)) (q27 (_ BitVec 7)) (q28 (_ BitVec 7)) (q29 (_ BitVec 7)) (q30 (_ BitVec 7)) (q31 (_ BitVec 7)) (q32 (_ BitVec 9))) (=> (distinct q26 q29) (bvsge (bvo
r q32 q32) (bvor q32 q32)))))
(assert (forall ((q33 (_ BitVec 7)) (q34 (_ BitVec 7)) (q35 (_ BitVec 7)) (q36 (_ BitVec 7)) (q37 (_ BitVec 7)) (q38 (_ BitVec 7)) (q39 (_ BitVec 7)) (q40 (_ BitVec 7)) (q41 (_ BitVec 7)) (q42 (_ BitVec 7
)) (q43 (_ BitVec 7)) (q44 (_ BitVec 7)) (q45 (_ BitVec 9))) (=> (= q36 q39) (bvugt (bvudiv q45 q45) q45))))
(assert (forall ((q46 (_ BitVec 7)) (q47 (_ BitVec 7)) (q48 (_ BitVec 8))) (=> (= q48 q48) (distinct (bvashr q47 (bvudiv q47 q46)) q46))))
(assert (forall ((q49 (_ BitVec 7)) (q50 (_ BitVec 7)) (q51 (_ BitVec 7)) (q52 (_ BitVec 7)) (q53 (_ BitVec 7)) (q54 (_ BitVec 7)) (q55 (_ BitVec 7)) (q56 (_ BitVec 7)) (q57 (_ BitVec 7)) (q58 (_ BitVec 7
)) (q59 (_ BitVec 7)) (q60 (_ BitVec 8))) (=> (bvuge q60 q60) (distinct q54 q56))))
(assert (forall ((q61 (_ BitVec 7)) (q62 (_ BitVec 7)) (q63 (_ BitVec 7)) (q64 (_ BitVec 7)) (q65 (_ BitVec 7)) (q66 (_ BitVec 7)) (q67 (_ BitVec 7)) (q68 (_ BitVec 7)) (q69 (_ BitVec 7)) (q70 (_ BitVec 7
)) (q71 (_ BitVec 7)) (q72 (_ BitVec 9))) (=> (= q71 q66) (= q72 (bvashr q72 q72)))))
(assert (forall ((q73 (_ BitVec 7)) (q74 (_ BitVec 7)) (q75 (_ BitVec 12))) (=> (bvule (bvsrem q75 q75) q75) (= (bvor (bvadd q73 q73) (bvnot q74)) q74))))
(declare-const bv_20-0 (_ BitVec 20))
(assert (forall ((q76 (_ BitVec 7)) (q77 (_ BitVec 7)) (q78 (_ BitVec 8))) (=> (bvsgt q76 (bvsub q76 (bvurem q76 q77))) (distinct (bvand q78 q78) q78))))
(assert (forall ((q79 (_ BitVec 7)) (q80 (_ BitVec 7)) (q81 (_ BitVec 7)) (q82 (_ BitVec 7)) (q83 (_ BitVec 7)) (q84 (_ BitVec 7)) (q85 (_ BitVec 9))) (=> (bvule q81 q80) (distinct (bvnor (bvurem q85 q85)
 q85) (bvnor (bvurem q85 q85) q85)))))
(assert (forall ((q86 (_ BitVec 7)) (q87 (_ BitVec 7)) (q88 (_ BitVec 7)) (q89 (_ BitVec 7)) (q90 (_ BitVec 7)) (q91 (_ BitVec 7)) (q92 (_ BitVec 7)) (q93 (_ BitVec 7)) (q94 (_ BitVec 7)) (q95 (_ BitVec 2
0))) (=> (distinct q88 q86) (bvsge (bvsub q95 q95) q95))))
(assert (forall ((q96 (_ BitVec 7)) (q97 (_ BitVec 7)) (q98 (_ BitVec 7)) (q99 (_ BitVec 7)) (q100 (_ BitVec 7)) (q101 (_ BitVec 7)) (q102 (_ BitVec 7)) (q103 (_ BitVec 7)) (q104 (_ BitVec 7)) (q105 (_ Bi
tVec 7)) (q106 (_ BitVec 3))) (=> (distinct q100 q96) (distinct q106 q106))))
(assert (forall ((q107 (_ BitVec 7)) (q108 (_ BitVec 7)) (q109 (_ BitVec 7)) (q110 (_ BitVec 7)) (q111 (_ BitVec 7)) (q112 (_ BitVec 7)) (q113 (_ BitVec 7)) (q114 (_ BitVec 7)) (q115 (_ BitVec 7)) (q116 (
_ BitVec 7)) (q117 (_ BitVec 12))) (=> (bvugt q115 q111) (bvsle (bvashr q117 q117) (bvashr q117 q117)))))
(assert (forall ((q118 (_ BitVec 7)) (q119 (_ BitVec 7)) (q120 (_ BitVec 7)) (q121 (_ BitVec 7)) (q122 (_ BitVec 7)) (q123 (_ BitVec 7)) (q124 (_ BitVec 7)) (q125 (_ BitVec 7)) (q126 (_ BitVec 7)) (q127 (
_ BitVec 7)) (q128 (_ BitVec 7)) (q129 (_ BitVec 7)) (q130 (_ BitVec 7)) (q131 (_ BitVec 9))) (=> (bvsle q122 q127) (= (bvnot (bvsmod q131 q131)) (bvsmod q131 q131)))))
(assert (forall ((q133 (_ BitVec 7)) (q134 (_ BitVec 8))) (=> (bvsle q133 (bvashr q133 q133)) (bvsgt q134 q134))))
(assert (forall ((q135 (_ BitVec 7)) (q136 (_ BitVec 7)) (q137 (_ BitVec 7)) (q138 (_ BitVec 7)) (q139 (_ BitVec 9))) (=> (= (bvand q137 q135) q136) (= q139 q139))))
(assert (forall ((q140 (_ BitVec 7)) (q141 (_ BitVec 7)) (q142 (_ BitVec 7)) (q143 (_ BitVec 7)) (q144 (_ BitVec 7)) (q145 (_ BitVec 7)) (q146 (_ BitVec 7)) (q147 (_ BitVec 7)) (q148 (_ BitVec 7)) (q149 (
_ BitVec 9))) (=> (bvule q146 q142) (distinct q149 (bvsrem q149 q149)))))
(assert (forall ((q150 (_ BitVec 7)) (q151 (_ BitVec 7)) (q152 (_ BitVec 7)) (q153 (_ BitVec 7)) (q154 Bool)) (=> (= q151 (bvadd q151 q153)) (or q154 q154 q154 q154 q154 q154))))
(assert (forall ((q155 (_ BitVec 7)) (q156 (_ BitVec 7)) (q157 (_ BitVec 7)) (q158 (_ BitVec 7)) (q159 (_ BitVec 7)) (q160 (_ BitVec 7)) (q161 (_ BitVec 7)) (q162 (_ BitVec 7)) (q163 (_ BitVec 7)) (q164 (
_ BitVec 7)) (q165 (_ BitVec 7)) (q166 (_ BitVec 7)) (q167 (_ BitVec 8))) (=> (= q167 (bvsdiv q167 q167)) (bvsge q164 q162))))
(assert (forall ((q168 (_ BitVec 7)) (q169 (_ BitVec 7)) (q170 (_ BitVec 7)) (q171 (_ BitVec 7)) (q172 (_ BitVec 7)) (q173 (_ BitVec 7)) (q174 (_ BitVec 7)) (q175 (_ BitVec 7)) (q176 (_ BitVec 7)) (q177 (
_ BitVec 7)) (q178 (_ BitVec 7)) (q179 (_ BitVec 7)) (q180 (_ BitVec 7)) (q181 (_ BitVec 7)) (q182 (_ BitVec 3))) (=> (= (bvsmod q182 q182) (bvsmod q182 q182)) (= q171 q176))))
(assert (forall ((q183 (_ BitVec 7)) (q184 (_ BitVec 7)) (q185 (_ BitVec 7)) (q186 (_ BitVec 7)) (q187 (_ BitVec 7)) (q188 (_ BitVec 7)) (q189 (_ BitVec 8))) (=> (bvugt q184 (bvashr q188 q186)) (= (bvashr
 q189 q189) q189))))
(assert (forall ((q190 (_ BitVec 7)) (q191 (_ BitVec 7)) (q192 (_ BitVec 7)) (q193 (_ BitVec 7)) (q194 (_ BitVec 7)) (q195 (_ BitVec 7)) (q196 (_ BitVec 7)) (q197 (_ BitVec 7)) (q198 (_ BitVec 7)) (q199 (
_ BitVec 7)) (q200 (_ BitVec 7)) (q201 (_ BitVec 7)) (q202 (_ BitVec 7)) (q203 (_ BitVec 7)) (q204 (_ BitVec 9))) (=> (bvugt (bvshl q204 q204) (bvshl q204 q204)) (distinct q203 q190))))
(assert (forall ((q205 (_ BitVec 7)) (q206 (_ BitVec 7)) (q207 (_ BitVec 7)) (q208 (_ BitVec 7)) (q209 (_ BitVec 7)) (q210 (_ BitVec 7)) (q211 (_ BitVec 7)) (q212 (_ BitVec 7)) (q213 (_ BitVec 7)) (q214 (
_ BitVec 7)) (q215 (_ BitVec 8))) (=> (distinct q210 q207) (= (bvnand q215 q215) q215))))
(assert (forall ((q216 (_ BitVec 7)) (q217 (_ BitVec 7)) (q218 (_ BitVec 7)) (q219 (_ BitVec 7)) (q220 (_ BitVec 3))) (=> (distinct q220 (bvlshr q220 q220)) (distinct q218 (bvsrem q219 q217)))))
(assert (forall ((q221 (_ BitVec 7)) (q222 (_ BitVec 7)) (q223 Bool)) (=> (distinct q221 (bvadd q221 q221)) (distinct q223 q223))))
(assert (forall ((q224 (_ BitVec 7)) (q225 (_ BitVec 7)) (q226 (_ BitVec 7)) (q227 (_ BitVec 7)) (q228 (_ BitVec 7)) (q229 Bool)) (=> (not q229) (= (bvshl (bvneg q228) q228) q227))))
(declare-const bv_25-0 (_ BitVec 25))
(assert (forall ((q238 (_ BitVec 7)) (q239 (_ BitVec 7)) (q240 (_ BitVec 7)) (q241 (_ BitVec 7)) (q242 (_ BitVec 7)) (q243 (_ BitVec 7)) (q244 (_ BitVec 7)) (q245 (_ BitVec 7)) (q246 (_ BitVec 7)) (q247 (
_ BitVec 7)) (q248 (_ BitVec 3))) (=> (= (bvor q248 q248) (bvashr (bvor q248 q248) (bvor q248 q248))) (= q242 q247))))
(assert (forall ((q249 (_ BitVec 7)) (q250 (_ BitVec 7)) (q251 (_ BitVec 7)) (q252 (_ BitVec 7)) (q253 (_ BitVec 7)) (q254 (_ BitVec 7)) (q255 (_ BitVec 7)) (q256 (_ BitVec 7)) (q257 (_ BitVec 7)) (q258 (
_ BitVec 7)) (q259 (_ BitVec 3))) (=> (distinct (bvmul q259 q259) q259) (bvslt q249 q250))))
(assert (forall ((q260 (_ BitVec 7)) (q261 (_ BitVec 7)) (q262 (_ BitVec 7)) (q263 (_ BitVec 7)) (q264 (_ BitVec 7)) (q265 (_ BitVec 7)) (q266 (_ BitVec 7)) (q267 (_ BitVec 7)) (q268 (_ BitVec 7)) (q269 (
_ BitVec 7)) (q270 (_ BitVec 7)) (q271 (_ BitVec 7)) (q272 (_ BitVec 7)) (q273 (_ BitVec 7)) (q274 (_ BitVec 10))) (=> (distinct q272 (bvsub q262 q266)) (distinct (bvmul (bvnot q274) (bvnot q274)) (bvnot 
q274)))))
(assert (forall ((q275 (_ BitVec 7)) (q276 (_ BitVec 7)) (q277 (_ BitVec 7)) (q278 (_ BitVec 7)) (q279 (_ BitVec 7)) (q280 (_ BitVec 7)) (q281 (_ BitVec 7)) (q282 (_ BitVec 7)) (q283 (_ BitVec 4))) (=> (b
vsgt q279 q278) (bvugt (bvurem q283 q283) (bvurem q283 q283)))))
(assert (forall ((q284 (_ BitVec 7)) (q285 (_ BitVec 25))) (=> (distinct q284 q284) (= q285 (bvashr q285 q285)))))
(assert (forall ((q286 (_ BitVec 7)) (q287 (_ BitVec 7)) (q288 (_ BitVec 7)) (q289 (_ BitVec 7)) (q290 (_ BitVec 7)) (q291 (_ BitVec 7)) (q292 (_ BitVec 7)) (q293 (_ BitVec 7)) (q294 (_ BitVec 7)) (q295 (
_ BitVec 7)) (q296 (_ BitVec 7)) (q297 (_ BitVec 7)) (q298 (_ BitVec 7)) (q299 (_ BitVec 7)) (q300 (_ BitVec 4))) (=> (= q300 (bvnand q300 q300)) (= (bvsmod q290 q297) q295))))
(assert (forall ((q301 (_ BitVec 7)) (q302 (_ BitVec 7)) (q303 (_ BitVec 7)) (q304 (_ BitVec 7)) (q305 (_ BitVec 7)) (q306 (_ BitVec 7)) (q307 (_ BitVec 10))) (=> (bvsle q307 q307) (bvsgt q305 q301))))
(assert (forall ((q314 (_ BitVec 7)) (q315 (_ BitVec 7)) (q316 (_ BitVec 7)) (q317 (_ BitVec 7)) (q318 (_ BitVec 7)) (q319 (_ BitVec 7)) (q320 (_ BitVec 7)) (q321 (_ BitVec 7)) (q322 (_ BitVec 7)) (q323 (
_ BitVec 7)) (q324 (_ BitVec 7)) (q325 (_ BitVec 7)) (q326 (_ BitVec 7)) (q327 (_ BitVec 7)) (q328 (_ BitVec 3))) (=> (bvsle (bvnand q328 q328) q328) (bvuge q324 q321))))
(assert (forall ((q329 (_ BitVec 7)) (q330 (_ BitVec 7)) (q331 (_ BitVec 7)) (q332 (_ BitVec 7)) (q333 (_ BitVec 7)) (q334 (_ BitVec 7)) (q335 (_ BitVec 7)) (q336 (_ BitVec 7)) (q337 (_ BitVec 20))) (=> (
bvuge q329 q336) (distinct q337 (bvshl q337 q337)))))
(assert (forall ((q338 (_ BitVec 7)) (q339 (_ BitVec 7)) (q340 (_ BitVec 7)) (q341 (_ BitVec 7)) (q342 (_ BitVec 7)) (q343 (_ BitVec 7)) (q344 (_ BitVec 7)) (q345 (_ BitVec 7)) (q346 (_ BitVec 7)) (q347 (
_ BitVec 7)) (q348 (_ BitVec 7)) (q349 (_ BitVec 7)) (q350 (_ BitVec 7)) (q351 (_ BitVec 7)) (q352 (_ BitVec 7)) (q353 (_ BitVec 3))) (=> (= q353 q353) (bvugt q341 q342))))
(declare-const bv_31-0 (_ BitVec 31))
(assert (forall ((q354 (_ BitVec 7)) (q355 (_ BitVec 7)) (q356 (_ BitVec 7)) (q357 (_ BitVec 7)) (q358 (_ BitVec 7)) (q359 (_ BitVec 7)) (q360 (_ BitVec 7)) (q361 (_ BitVec 7)) (q362 (_ BitVec 10))) (=> (
= q357 (bvnor q361 q358)) (bvult (bvadd (bvlshr q362 q362) q362) (bvadd (bvlshr q362 q362) q362)))))
(assert (forall ((q363 (_ BitVec 7)) (q364 (_ BitVec 7)) (q365 (_ BitVec 7)) (q366 (_ BitVec 7)) (q367 (_ BitVec 20))) (=> (bvsle (bvurem q367 q367) (bvurem q367 q367)) (distinct q366 q363))))
(assert (forall ((q368 (_ BitVec 7)) (q369 (_ BitVec 3))) (=> (distinct q369 q369) (bvuge (bvadd q368 q368) (bvadd q368 q368)))))
(assert (forall ((q370 (_ BitVec 7)) (q371 (_ BitVec 7)) (q372 (_ BitVec 7)) (q373 (_ BitVec 7)) (q374 (_ BitVec 7)) (q375 (_ BitVec 7)) (q376 (_ BitVec 7)) (q377 (_ BitVec 3))) (=> (distinct q375 q372) (
= (bvshl (bvsmod q377 q377) (bvsmod q377 q377)) (bvsmod q377 q377)))))
(declare-const bv_24-0 (_ BitVec 24))
(assert (forall ((q395 (_ BitVec 7)) (q396 (_ BitVec 7)) (q397 (_ BitVec 7)) (q398 (_ BitVec 7)) (q399 (_ BitVec 7)) (q400 (_ BitVec 7)) (q401 (_ BitVec 7)) (q402 (_ BitVec 20))) (=> (bvult q401 q397) (= 
q402 (bvsrem q402 q402)))))
(assert (forall ((q403 (_ BitVec 7)) (q404 (_ BitVec 7)) (q405 (_ BitVec 7)) (q406 (_ BitVec 7)) (q407 (_ BitVec 7)) (q408 (_ BitVec 7)) (q409 (_ BitVec 7)) (q410 (_ BitVec 7)) (q411 (_ BitVec 7)) (q412 (
_ BitVec 7)) (q413 (_ BitVec 7)) (q414 (_ BitVec 8))) (=> (= q409 q408) (distinct (bvadd q414 (bvsdiv q414 q414)) (bvsdiv q414 q414)))))
(assert (forall ((q415 (_ BitVec 7)) (q416 (_ BitVec 7)) (q417 (_ BitVec 7)) (q418 (_ BitVec 7)) (q419 (_ BitVec 7)) (q420 (_ BitVec 7)) (q421 (_ BitVec 7)) (q422 (_ BitVec 7)) (q423 (_ BitVec 7)) (q424 (
_ BitVec 7)) (q425 (_ BitVec 31))) (=> (= q422 q419) (distinct (bvshl q425 q425) (bvshl q425 q425)))))
(assert (forall ((q426 (_ BitVec 7)) (q427 (_ BitVec 7)) (q428 (_ BitVec 7)) (q429 (_ BitVec 7)) (q430 (_ BitVec 7)) (q431 (_ BitVec 7)) (q432 (_ BitVec 7)) (q433 (_ BitVec 7)) (q434 (_ BitVec 7)) (q435 (
_ BitVec 7)) (q436 (_ BitVec 4))) (=> (bvule (bvashr q436 q436) (bvashr q436 q436)) (= q428 (bvsrem q433 q432)))))
(assert (forall ((q437 (_ BitVec 7)) (q438 (_ BitVec 7)) (q439 (_ BitVec 7)) (q440 (_ BitVec 7)) (q441 (_ BitVec 7)) (q442 (_ BitVec 7)) (q443 (_ BitVec 7)) (q444 (_ BitVec 7)) (q445 (_ BitVec 7)) (q446 (
_ BitVec 7)) (q447 (_ BitVec 7)) (q448 (_ BitVec 7)) (q449 (_ BitVec 7)) (q450 (_ BitVec 20))) (=> (= q450 (bvshl q450 q450)) (= q438 q443))))
(assert (forall ((q451 (_ BitVec 7)) (q452 (_ BitVec 7)) (q453 (_ BitVec 7)) (q454 (_ BitVec 7)) (q455 (_ BitVec 7)) (q456 (_ BitVec 7)) (q457 (_ BitVec 7)) (q458 (_ BitVec 7)) (q459 (_ BitVec 7)) (q460 (
_ BitVec 7)) (q461 (_ BitVec 7)) (q462 (_ BitVec 7)) (q463 (_ BitVec 7)) (q464 (_ BitVec 7)) (q465 (_ BitVec 7)) (q466 (_ BitVec 12))) (=> (bvugt q452 q457) (bvsgt q466 q466))))
(assert (forall ((q467 (_ BitVec 7)) (q468 (_ BitVec 7)) (q469 (_ BitVec 7)) (q470 (_ BitVec 7)) (q471 (_ BitVec 7)) (q472 (_ BitVec 7)) (q473 (_ BitVec 7)) (q474 (_ BitVec 10))) (=> (= (bvnor q474 q474) 
(bvnor q474 q474)) (= (bvmul q473 (bvshl q470 q473)) q469))))
(assert (forall ((q475 (_ BitVec 7)) (q476 (_ BitVec 7)) (q477 (_ BitVec 7)) (q478 (_ BitVec 7)) (q479 (_ BitVec 7)) (q480 (_ BitVec 7)) (q481 (_ BitVec 7)) (q482 (_ BitVec 7)) (q483 (_ BitVec 7)) (q484 (
_ BitVec 7)) (q485 Bool)) (=> (and q485 q485 q485 q485 q485 q485) (bvsge (bvnot q484) (bvnot q484)))))
(check-sat)

'-assert', '-noSlicing', '-abstract:oct'

Theories: GroebnerMultiplication, ModuloArithmetic
 Exception in thread "main" java.lang.AssertionError: assertion failed
        at scala.Predef$.assert(Predef.scala:156)
        at lazabs.horn.bottomup.HornWrapper$.verifyCEX(HornWrapper.scala:102)
        at lazabs.horn.bottomup.InnerHornWrapper.<init>(HornWrapper.scala:443)
        at lazabs.horn.bottomup.HornWrapper$$anonfun$11.apply(HornWrapper.scala:254)
        at lazabs.horn.bottomup.HornWrapper$$anonfun$11.apply(HornWrapper.scala:256)
        at lazabs.ParallelComputation$.apply(ParallelComputation.scala:46)
        at lazabs.horn.bottomup.HornWrapper.<init>(HornWrapper.scala:253)
        at lazabs.horn.Solve$.apply(Solve.scala:81)
        at lazabs.Main$.doMain(Main.scala:601)
        at lazabs.Main$.main(Main.scala:271)
        at lazabs.Main.main(Main.scala)

(set-logic HORN)
(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const bv_2-0 (_ BitVec 2))
(declare-const bv_5-0 (_ BitVec 5))
(declare-const bv_3-0 (_ BitVec 3))
(assert (forall ((q0 (_ BitVec 2)) (q1 (_ BitVec 9))) (=> (= q1 q1) (bvsge (bvsdiv q0 q0) (bvsdiv q0 q0)))))
(assert (forall ((q2 (_ BitVec 2)) (q3 (_ BitVec 2)) (q4 (_ BitVec 2)) (q5 (_ BitVec 2)) (q6 (_ BitVec 10))) (=> (= (bvurem q2 q5) q3) (= q6 q6))))
(assert (forall ((q15 (_ BitVec 2)) (q16 (_ BitVec 10))) (=> (bvugt (bvneg q15) q15) (= (bvor (bvmul q16 q16) (bvashr q16 (bvmul q16 q16))) (bvor (bvmul q16 q16) (bvashr q16 (bvmul q16 q16)))))))
(check-sat)

Theories: GroebnerMultiplication, ModuloArithmetic
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:433)
	at lazabs.horn.bottomup.HornWrapper$$anonfun$11.apply(HornWrapper.scala:254)
	at lazabs.horn.bottomup.HornWrapper$$anonfun$11.apply(HornWrapper.scala:256)
	at lazabs.ParallelComputation$.apply(ParallelComputation.scala:46)
	at lazabs.horn.bottomup.HornWrapper.<init>(HornWrapper.scala:253)
	at lazabs.horn.Solve$.apply(Solve.scala:81)
	at lazabs.Main$.doMain(Main.scala:601)
	at lazabs.Main$.main(Main.scala:271)
	at lazabs.Main.main(Main.scala)

(declare-datatype f_type ((cons (b Int))))
(declare-datatype abi_type ((a)))

(declare-fun pred1 (Int abi_type f_type f_type) Bool)

(assert (forall ((l abi_type) (p f_type)) (pred1 0 l p p)))
(assert (forall ((m abi_type) (o Int) (aa f_type) (ab f_type))
  (=> (pred1 o m aa ab) (or (exists ((var0 abi_type)) (not (= var0 a))) (and (= ab aa) (= o 0)))))
)

(check-sat)

$ ~/eldarica/eld  sat.smt2 
unsat

(set-logic HORN)
(assert (forall ((q0 (_ BitVec 12)) (q1 (_ BitVec 12)) (q2 (_ BitVec 32))) (=> (= q1 q0) (bvslt (bvurem (bvsrem (bvsrem q2 q2) q2) q2) q2))))
(assert (forall ((q3 (_ BitVec 12)) (q4 (_ BitVec 12)) (q5 (_ BitVec 12)) (q6 (_ BitVec 12)) (q7 (_ BitVec 12)) (q8 (_ BitVec 12)) (q9 (_ BitVec 12)) (q10 (_ BitVec 12)) (q11 (_ BitVec 12)) (q12 (_ BitVec 12)) (q13 (_ BitVec 12)) (q14 (_ BitVec 12)) (q15 (_ BitVec 12)) (q16 (_ BitVec 10))) (=> (= q14 q8) (distinct q16 (bvnot q16)))))
(assert (forall ((q17 (_ BitVec 12)) (q18 (_ BitVec 12)) (q19 (_ BitVec 12)) (q20 (_ BitVec 12)) (q21 (_ BitVec 12)) (q22 (_ BitVec 12)) (q23 (_ BitVec 12)) (q24 (_ BitVec 32))) (=> (distinct q24 (bvsdiv q24 q24)) (= (bvsmod q19 q17) q17))))
(assert (forall ((q25 (_ BitVec 12)) (q26 (_ BitVec 12)) (q27 (_ BitVec 12)) (q28 (_ BitVec 12)) (q29 (_ BitVec 12)) (q30 (_ BitVec 12)) (q31 (_ BitVec 12)) (q32 (_ BitVec 20))) (=> (= q32 (bvnand q32 q32)) (= q25 q26))))
(assert (forall ((q33 (_ BitVec 12)) (q34 (_ BitVec 12)) (q35 (_ BitVec 12)) (q36 (_ BitVec 12)) (q37 (_ BitVec 12)) (q38 (_ BitVec 12)) (q39 (_ BitVec 12)) (q40 (_ BitVec 12)) (q41 (_ BitVec 7))) (=> (bvuge (bvsdiv q41 q41) (bvsdiv q41 q41)) (distinct q33 q38))))
(assert (forall ((q42 (_ BitVec 12)) (q43 (_ BitVec 12)) (q44 (_ BitVec 12)) (q45 (_ BitVec 12)) (q46 (_ BitVec 12)) (q47 (_ BitVec 12)) (q48 (_ BitVec 12)) (q49 (_ BitVec 12)) (q50 (_ BitVec 12)) (q51 (_ BitVec 12)) (q52 (_ BitVec 12)) (q53 (_ BitVec 12)) (q54 (_ BitVec 12)) (q55 (_ BitVec 7))) (=> (distinct q54 q53) (= (bvsmod (bvneg q55) (bvneg q55)) (bvneg q55)))))
(assert (forall ((q56 (_ BitVec 12)) (q57 (_ BitVec 12)) (q58 (_ BitVec 39))) (=> (= q58 ((_ sign_extend 0) q58)) (bvult (bvudiv q56 q57) (bvlshr (bvudiv q56 q57) q56)))))
(assert (forall ((q59 (_ BitVec 12)) (q60 (_ BitVec 12)) (q61 (_ BitVec 39))) (=> (distinct q61 q61) (bvsge (bvudiv q60 q60) (bvsub q60 q59)))))
(assert (forall ((q62 (_ BitVec 12)) (q63 (_ BitVec 12)) (q64 (_ BitVec 12)) (q65 (_ BitVec 12)) (q66 (_ BitVec 12)) (q67 (_ BitVec 12)) (q68 Bool)) (=> (= q63 q62) (=> q68 q68))))
(assert (forall ((q69 (_ BitVec 12)) (q70 (_ BitVec 12)) (q71 (_ BitVec 12)) (q72 (_ BitVec 12)) (q73 (_ BitVec 12)) (q74 (_ BitVec 12)) (q75 (_ BitVec 12)) (q76 (_ BitVec 12)) (q77 (_ BitVec 12)) (q78 (_ BitVec 12)) (q79 (_ BitVec 12)) (q80 (_ BitVec 12)) (q81 (_ BitVec 12)) (q82 Bool)) (=> (distinct q80 q74) (xor q82 q82 q82 q82 q82 q82))))
(assert (forall ((q83 (_ BitVec 12)) (q84 (_ BitVec 12)) (q85 (_ BitVec 12)) (q86 (_ BitVec 12)) (q87 (_ BitVec 12)) (q88 (_ BitVec 12)) (q89 (_ BitVec 12)) (q90 (_ BitVec 12)) (q91 (_ BitVec 7))) (=> (= q85 q88) (= q91 (bvnand q91 q91)))))
(assert (forall ((q92 (_ BitVec 12)) (q93 (_ BitVec 12)) (q94 (_ BitVec 12)) (q95 (_ BitVec 12)) (q96 (_ BitVec 12)) (q97 (_ BitVec 12)) (q98 (_ BitVec 12)) (q99 (_ BitVec 39))) (=> (bvsge (bvand q99 q99) q99) (bvsgt q92 q92))))
(assert (forall ((q100 (_ BitVec 12)) (q101 (_ BitVec 12)) (q102 (_ BitVec 12)) (q103 (_ BitVec 12)) (q104 (_ BitVec 12)) (q105 (_ BitVec 12)) (q106 (_ BitVec 12)) (q107 (_ BitVec 8))) (=> (= q107 (bvnand q107 q107)) (distinct q100 q102))))
(assert (forall ((q108 (_ BitVec 12)) (q109 (_ BitVec 12)) (q110 (_ BitVec 12)) (q111 (_ BitVec 12)) (q112 (_ BitVec 12)) (q113 (_ BitVec 12)) (q114 (_ BitVec 12)) (q115 (_ BitVec 12)) (q116 (_ BitVec 12)) (q117 (_ BitVec 12)) (q118 (_ BitVec 12)) (q119 (_ BitVec 12)) (q120 (_ BitVec 12)) (q121 (_ BitVec 8))) (=> (= q111 (bvsub q110 q119)) (distinct q121 (bvashr q121 q121)))))
(assert (forall ((q122 (_ BitVec 12)) (q123 (_ BitVec 12)) (q124 (_ BitVec 12)) (q125 (_ BitVec 12)) (q126 (_ BitVec 12)) (q127 (_ BitVec 12)) (q128 (_ BitVec 12)) (q129 (_ BitVec 12)) (q130 (_ BitVec 12)) (q131 (_ BitVec 12)) (q132 (_ BitVec 8))) (=> (distinct q125 q126) (distinct (bvurem q132 q132) (bvnor q132 q132)))))
(assert (forall ((q133 (_ BitVec 12)) (q134 (_ BitVec 12)) (q135 (_ BitVec 12)) (q136 (_ BitVec 12)) (q137 (_ BitVec 12)) (q138 (_ BitVec 12)) (q139 (_ BitVec 12)) (q140 (_ BitVec 12)) (q141 (_ BitVec 12)) (q142 (_ BitVec 12)) (q143 (_ BitVec 12)) (q144 Bool)) (=> (bvsgt q136 q141) (or q144 q144 q144 q144))))
(assert (forall ((q159 (_ BitVec 12)) (q160 (_ BitVec 12)) (q161 (_ BitVec 12)) (q162 (_ BitVec 12)) (q163 (_ BitVec 12)) (q164 (_ BitVec 12)) (q165 (_ BitVec 8))) (=> (= (bvsub q162 q159) (bvsub q162 q159)) (distinct (bvsub q165 q165) (bvsub q165 q165)))))
(assert (forall ((q166 (_ BitVec 12)) (q167 (_ BitVec 12)) (q168 (_ BitVec 12)) (q169 (_ BitVec 12)) (q170 (_ BitVec 12)) (q171 (_ BitVec 12)) (q172 (_ BitVec 32))) (=> (bvsle q172 (bvadd q172 q172)) (bvsge q171 q168))))
(assert (forall ((q173 (_ BitVec 12)) (q174 (_ BitVec 12)) (q175 (_ BitVec 12)) (q176 (_ BitVec 12)) (q177 (_ BitVec 12)) (q178 (_ BitVec 12)) (q179 (_ BitVec 12)) (q180 (_ BitVec 12)) (q181 (_ BitVec 12)) (q182 (_ BitVec 7))) (=> (= q178 q180) (distinct q182 q182))))
(assert (forall ((q183 (_ BitVec 12)) (q184 (_ BitVec 12)) (q185 (_ BitVec 10))) (=> (bvslt q185 q185) (= q184 q183))))
(assert (forall ((q186 (_ BitVec 12)) (q187 (_ BitVec 12)) (q188 (_ BitVec 12)) (q189 (_ BitVec 12)) (q190 (_ BitVec 12)) (q191 (_ BitVec 12)) (q192 (_ BitVec 12)) (q193 (_ BitVec 12)) (q194 (_ BitVec 12)) (q195 (_ BitVec 12)) (q196 (_ BitVec 12)) (q197 (_ BitVec 12)) (q198 (_ BitVec 12)) (q199 (_ BitVec 12)) (q200 (_ BitVec 31))) (=> (bvslt q196 q195) (= q200 (bvnot q200)))))
(assert (forall ((q201 (_ BitVec 12)) (q202 (_ BitVec 12)) (q203 (_ BitVec 12)) (q204 (_ BitVec 12)) (q205 (_ BitVec 12)) (q206 (_ BitVec 12)) (q207 (_ BitVec 12)) (q208 (_ BitVec 12)) (q209 (_ BitVec 39))) (=> (bvsgt q209 q209) (= (bvnor q202 (bvadd q207 q206)) (bvshl q201 q208)))))
(assert (forall ((q210 (_ BitVec 12)) (q211 (_ BitVec 12)) (q212 (_ BitVec 12)) (q213 (_ BitVec 12)) (q214 (_ BitVec 12)) (q215 (_ BitVec 12)) (q216 (_ BitVec 12)) (q217 (_ BitVec 12)) (q218 (_ BitVec 12)) (q219 (_ BitVec 12)) (q220 (_ BitVec 31))) (=> (bvult q211 q219) (distinct (bvsrem q220 q220) (bvurem (bvsrem q220 q220) q220)))))
(assert (forall ((q221 (_ BitVec 12)) (q222 (_ BitVec 12)) (q223 (_ BitVec 12)) (q224 (_ BitVec 12)) (q225 (_ BitVec 12)) (q226 (_ BitVec 12)) (q227 (_ BitVec 12)) (q228 (_ BitVec 12)) (q229 (_ BitVec 12)) (q230 (_ BitVec 12)) (q231 (_ BitVec 12)) (q232 (_ BitVec 12)) (q233 (_ BitVec 10))) (=> (distinct q231 q223) (distinct (bvnand (bvmul q233 q233) q233) (bvor (bvmul q233 q233) (bvnand (bvmul q233 q233) q233))))))
(assert (forall ((q253 (_ BitVec 12)) (q254 (_ BitVec 12)) (q255 (_ BitVec 12)) (q256 (_ BitVec 12)) (q257 (_ BitVec 7))) (=> (= (bvsdiv q253 q255) q253) (= (bvudiv q257 q257) (bvudiv q257 q257)))))
(assert (forall ((q258 (_ BitVec 12)) (q259 (_ BitVec 12)) (q260 (_ BitVec 12)) (q261 (_ BitVec 12)) (q262 (_ BitVec 12)) (q263 (_ BitVec 12)) (q264 (_ BitVec 12)) (q265 (_ BitVec 12)) (q266 (_ BitVec 12)) (q267 (_ BitVec 12)) (q268 (_ BitVec 12)) (q269 (_ BitVec 12)) (q270 (_ BitVec 12)) (q271 (_ BitVec 7))) (=> (= q270 q261) (bvslt q271 (bvashr q271 q271)))))
(assert (forall ((q272 (_ BitVec 12)) (q273 (_ BitVec 12)) (q274 (_ BitVec 12)) (q275 (_ BitVec 12)) (q276 (_ BitVec 12)) (q277 (_ BitVec 12)) (q278 (_ BitVec 12)) (q279 (_ BitVec 12)) (q280 (_ BitVec 12)) (q281 Bool)) (=> (and q281 q281 q281 q281 q281 q281 q281 q281 q281) (= q279 q275))))
(assert (forall ((q282 (_ BitVec 12)) (q283 (_ BitVec 12)) (q284 (_ BitVec 12)) (q285 (_ BitVec 12)) (q286 (_ BitVec 12)) (q287 (_ BitVec 12)) (q288 (_ BitVec 12)) (q289 (_ BitVec 12)) (q290 (_ BitVec 12)) (q291 (_ BitVec 20))) (=> (= (bvsdiv q291 q291) q291) (= q286 (bvor q290 q289)))))
(assert (forall ((q293 (_ BitVec 12)) (q294 (_ BitVec 12)) (q295 (_ BitVec 12)) (q296 (_ BitVec 12)) (q297 (_ BitVec 12)) (q298 Bool)) (=> (not q298) (= q294 q293))))
(assert (forall ((q299 (_ BitVec 12)) (q300 (_ BitVec 12)) (q301 (_ BitVec 12)) (q302 (_ BitVec 8))) (=> (bvult q302 q302) (bvsge q301 q301))))
(assert (forall ((q303 (_ BitVec 12)) (q304 (_ BitVec 12)) (q305 (_ BitVec 12)) (q306 (_ BitVec 12)) (q307 (_ BitVec 12)) (q308 (_ BitVec 12)) (q309 (_ BitVec 7))) (=> (distinct q305 q303) (bvslt q309 q309))))
(assert (forall ((q310 (_ BitVec 12)) (q311 (_ BitVec 12)) (q312 (_ BitVec 12)) (q313 (_ BitVec 12)) (q314 (_ BitVec 12)) (q315 (_ BitVec 31))) (=> (= (bvshl q314 q314) (bvshl q314 q314)) (distinct q315 q315))))
(assert (forall ((q316 (_ BitVec 12)) (q317 (_ BitVec 12)) (q318 (_ BitVec 12)) (q319 (_ BitVec 12)) (q320 (_ BitVec 12)) (q321 (_ BitVec 12)) (q322 (_ BitVec 12)) (q323 (_ BitVec 12)) (q324 (_ BitVec 12)) (q325 (_ BitVec 12)) (q326 (_ BitVec 12)) (q327 (_ BitVec 12)) (q328 (_ BitVec 20))) (=> (= q323 (bvnor q325 q326)) (distinct (bvashr (bvsub q328 q328) q328) q328))))
(assert (forall ((q330 (_ BitVec 12)) (q331 (_ BitVec 12)) (q332 (_ BitVec 9))) (=> (bvsgt q330 (bvshl q330 q331)) (distinct q332 q332))))
(assert (forall ((q333 (_ BitVec 12)) (q334 (_ BitVec 12)) (q335 (_ BitVec 12)) (q336 (_ BitVec 12)) (q337 (_ BitVec 12)) (q338 (_ BitVec 12)) (q339 (_ BitVec 12)) (q340 (_ BitVec 12)) (q341 (_ BitVec 12)) (q342 (_ BitVec 15))) (=> (distinct q338 q336) (= (bvlshr q342 q342) (bvlshr q342 q342)))))
(assert (forall ((q343 (_ BitVec 12)) (q344 (_ BitVec 12)) (q345 (_ BitVec 12)) (q346 (_ BitVec 12)) (q347 (_ BitVec 12)) (q348 (_ BitVec 31))) (=> (= q348 (bvand q348 (bvsmod q348 q348))) (distinct q347 q344))))
(assert (forall ((q349 (_ BitVec 12)) (q350 (_ BitVec 12)) (q351 (_ BitVec 12)) (q352 (_ BitVec 12)) (q353 (_ BitVec 12)) (q354 (_ BitVec 12)) (q355 (_ BitVec 12)) (q356 (_ BitVec 12)) (q357 (_ BitVec 12)) (q358 (_ BitVec 12)) (q359 (_ BitVec 12)) (q360 (_ BitVec 12)) (q361 (_ BitVec 8))) (=> (bvslt (bvor q361 q361) (bvor q361 q361)) (bvsle q360 q353))))
(assert (forall ((q362 (_ BitVec 12)) (q363 (_ BitVec 12)) (q364 (_ BitVec 12)) (q365 (_ BitVec 12)) (q366 (_ BitVec 12)) (q367 (_ BitVec 12)) (q368 (_ BitVec 12)) (q369 (_ BitVec 12)) (q370 (_ BitVec 39))) (=> (= (bvsrem q370 q370) (bvsrem q370 q370)) (distinct q368 q367))))
(assert (forall ((q371 (_ BitVec 12)) (q372 (_ BitVec 12)) (q373 (_ BitVec 12)) (q374 (_ BitVec 12)) (q375 (_ BitVec 12)) (q376 (_ BitVec 12)) (q377 (_ BitVec 12)) (q378 (_ BitVec 12)) (q379 (_ BitVec 12)) (q380 (_ BitVec 12)) (q381 (_ BitVec 12)) (q382 (_ BitVec 12)) (q383 (_ BitVec 10))) (=> (= q383 (bvashr q383 q383)) (distinct q371 (bvnot (bvsdiv q375 q375))))))
(assert (forall ((q384 (_ BitVec 12)) (q385 (_ BitVec 12)) (q386 (_ BitVec 12)) (q387 (_ BitVec 12)) (q388 (_ BitVec 9))) (=> (distinct q385 q385) (= (bvshl q388 q388) (bvadd q388 q388)))))
(assert (forall ((q389 (_ BitVec 12)) (q390 (_ BitVec 12)) (q391 (_ BitVec 12)) (q392 Bool)) (=> (distinct q392 q392 q392 q392 q392 q392 q392 q392 q392) (= q390 (bvlshr q391 (bvshl q390 q390))))))
(assert (forall ((q393 (_ BitVec 12)) (q394 (_ BitVec 12)) (q395 (_ BitVec 12)) (q396 (_ BitVec 12)) (q397 (_ BitVec 12)) (q398 (_ BitVec 12)) (q399 (_ BitVec 12)) (q400 (_ BitVec 12)) (q401 (_ BitVec 12)) (q402 (_ BitVec 12)) (q403 (_ BitVec 12)) (q404 (_ BitVec 12)) (q405 (_ BitVec 12)) (q406 (_ BitVec 12)) (q407 (_ BitVec 1))) (=> (distinct q407 q407) (bvsgt q402 q395))))
(assert (forall ((q409 (_ BitVec 12)) (q410 (_ BitVec 12)) (q411 (_ BitVec 12)) (q412 (_ BitVec 12)) (q413 (_ BitVec 12)) (q414 (_ BitVec 12)) (q415 (_ BitVec 12)) (q416 (_ BitVec 12)) (q417 (_ BitVec 12)) (q418 (_ BitVec 12)) (q419 (_ BitVec 12)) (q420 (_ BitVec 12)) (q421 (_ BitVec 12)) (q422 Bool)) (=> (distinct q409 q411) (and q422 q422 q422 q422 q422))))
(assert (forall ((q423 (_ BitVec 12)) (q424 (_ BitVec 12)) (q425 (_ BitVec 12)) (q426 (_ BitVec 12)) (q427 (_ BitVec 12)) (q428 (_ BitVec 12)) (q429 (_ BitVec 12)) (q430 (_ BitVec 12)) (q431 (_ BitVec 12)) (q432 (_ BitVec 12)) (q433 (_ BitVec 12)) (q434 (_ BitVec 12)) (q435 (_ BitVec 12)) (q436 (_ BitVec 20))) (=> (= q426 q426) (distinct q436 q436))))
(assert (forall ((q438 (_ BitVec 12)) (q439 (_ BitVec 12)) (q440 (_ BitVec 12)) (q441 (_ BitVec 12)) (q442 (_ BitVec 12)) (q443 (_ BitVec 12)) (q444 (_ BitVec 8))) (=> (bvugt q443 q439) (bvslt (bvsdiv q444 q444) (bvsdiv q444 q444)))))
(assert (forall ((q445 (_ BitVec 12)) (q446 (_ BitVec 12)) (q447 (_ BitVec 12)) (q448 (_ BitVec 12)) (q449 (_ BitVec 12)) (q450 (_ BitVec 12)) (q451 (_ BitVec 12)) (q452 (_ BitVec 12)) (q453 (_ BitVec 12)) (q454 (_ BitVec 12)) (q455 (_ BitVec 12)) (q456 (_ BitVec 12)) (q457 (_ BitVec 12)) (q458 (_ BitVec 9))) (=> (= q458 (bvsub (bvand q458 q458) q458)) (bvuge q447 q445))))
(assert (forall ((q459 (_ BitVec 12)) (q460 (_ BitVec 12)) (q461 (_ BitVec 12)) (q462 (_ BitVec 12)) (q463 (_ BitVec 12)) (q464 (_ BitVec 12)) (q465 (_ BitVec 12)) (q466 (_ BitVec 12)) (q467 (_ BitVec 20))) (=> (distinct q461 q466) (bvule (bvsmod q467 (bvsub q467 q467)) (bvsub q467 q467)))))
(check-sat)

Theories: GroebnerMultiplication, ModuloArithmetic
 (error "Internal exception: java.lang.AssertionError: assertion failed")

Theories: GroebnerMultiplication, ModuloArithmetic
 Exception in thread "main" java.lang.AssertionError: assertion failed
 	at scala.Predef$.assert(Predef.scala:156)
 	at ap.terfor.arithconj.InNegEqModelElement.extendModel(ModelFinder.scala:298)
 	at ap.terfor.arithconj.ModelElement$$anonfun$constructModel$1.apply(ModelFinder.scala:55)
 	at ap.terfor.arithconj.ModelElement$$anonfun$constructModel$1.apply(ModelFinder.scala:55)
 	at scala.collection.immutable.List.foreach(List.scala:392)
 	at ap.terfor.arithconj.ModelElement$.constructModel(ModelFinder.scala:55)
 	at ap.proof.ModelSearchProver.extractModel$1(ModelSearchProver.scala:730)
 	at ap.proof.ModelSearchProver.handleSatGoal(ModelSearchProver.scala:852)
 	at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:482)
 	at ap.proof.ModelSearchProver.extractModel$1(ModelSearchProver.scala:772)
 	at ap.proof.ModelSearchProver.handleSatGoal(ModelSearchProver.scala:852)
 	at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:482)
 	at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:476)
 	at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:476)
 	at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:476)
 	at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:589)
 	at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:589)
 	at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:476)
 	at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:476)
 	at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:589)
 	at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:589)
 	at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:476)
 	at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:476)
 	at ap.proof.ModelSearchProver$IncProverImpl.checkValidityDir(ModelSearchProver.scala:1079)
 	at ap.proof.ModelSearchProver$IncProverImpl.checkValidityDir(ModelSearchProver.scala:1069)
 	at ap.proof.ModelSearchProver$IncProverImpl.checkValidity(ModelSearchProver.scala:1057)
 	at lazabs.horn.bottomup.HornPredAbs$$anonfun$isValid$1.apply$mcZ$sp(HornPredAbs.scala:705)
 	at lazabs.horn.bottomup.HornPredAbs$$anonfun$isValid$1.apply(HornPredAbs.scala:696)
 	at lazabs.horn.bottomup.HornPredAbs$$anonfun$isValid$1.apply(HornPredAbs.scala:696)
 	at scala.util.DynamicVariable.withValue(DynamicVariable.scala:58)
 	at ap.util.Timeout$.withChecker(Timeout.scala:44)
 	at lazabs.horn.bottomup.HornPredAbs.isValid(HornPredAbs.scala:696)
 	at lazabs.horn.bottomup.HornPredAbs$$anonfun$genEdge$1.apply(HornPredAbs.scala:1459)
 	at lazabs.horn.bottomup.HornPredAbs$$anonfun$genEdge$1.apply(HornPredAbs.scala:1450)
 	at lazabs.horn.bottomup.Hasher.scope(Hasher.scala:356)
 	at lazabs.horn.bottomup.HornPredAbs.genEdge(HornPredAbs.scala:1450)
 	at lazabs.horn.bottomup.HornPredAbs.liftedTree1$1(HornPredAbs.scala:872)
 	at lazabs.horn.bottomup.HornPredAbs.<init>(HornPredAbs.scala:871)
 	at lazabs.horn.bottomup.InnerHornWrapper$$anonfun$26.apply(HornWrapper.scala:398)
 	at lazabs.horn.bottomup.InnerHornWrapper$$anonfun$26.apply(HornWrapper.scala:392)
 	at scala.util.DynamicVariable.withValue(DynamicVariable.scala:58)
 	at scala.Console$.withOut(Console.scala:65)
 	at lazabs.horn.bottomup.InnerHornWrapper.<init>(HornWrapper.scala:392)
 	at lazabs.horn.bottomup.HornWrapper$$anonfun$11.apply(HornWrapper.scala:254)
 	at lazabs.horn.bottomup.HornWrapper$$anonfun$11.apply(HornWrapper.scala:256)
 	at lazabs.ParallelComputation$.apply(ParallelComputation.scala:46)
 	at lazabs.horn.bottomup.HornWrapper.<init>(HornWrapper.scala:253)
 	at lazabs.horn.Solve$.apply(Solve.scala:81)
 	at lazabs.Main$.doMain(Main.scala:601)
 	at lazabs.Main$.main(Main.scala:271)
 	at lazabs.Main.main(Main.scala)

(set-logic HORN)
(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const bv_14-0 (_ BitVec 14))
(assert (forall ((q0 (_ BitVec 12)) (q1 (_ BitVec 12)) (q2 (_ BitVec 12)) (q3 (_ BitVec 12)) (q4 (_ BitVec 12)) (q5 (_ BitVec 12)) (q6 (_ BitVec 12)) (q7 (_ BitVec 12)) (q8 (_ BitVec 12)) (q9 (_ BitVec 12)) (q10 (_ BitVec 12)) (q11 (_ BitVec 12)) (q12 (_ BitVec 12)) (q13 (_ BitVec 12)) (q14 (_ BitVec 12)) (q15 (_ BitVec 12)) (q16 (_ BitVec 12)) (q17 (_ BitVec 12)) (q18 (_ BitVec 12)) (q19 (_ BitVec 12)) (q20 (_ BitVec 12)) (q21 (_ BitVec 14))) (=> (distinct q16 q2) (bvsgt (bvsrem (bvudiv q21 q21) (bvashr q21 q21)) (bvashr q21 q21)))))
(assert (forall ((q22 (_ BitVec 12)) (q23 (_ BitVec 12)) (q24 (_ BitVec 12)) (q25 (_ BitVec 12)) (q26 (_ BitVec 12)) (q27 Bool)) (=> (distinct (bvsub q23 q24) q26) (=> q27 q27))))
(assert (forall ((q28 (_ BitVec 12)) (q29 (_ BitVec 12)) (q30 (_ BitVec 12)) (q31 (_ BitVec 12)) (q32 (_ BitVec 12)) (q33 (_ BitVec 12)) (q34 Bool)) (=> (xor q34 q34 q34 q34 q34 q34) (= q30 (bvashr q33 q29)))))
(assert (forall ((q35 (_ BitVec 12)) (q36 (_ BitVec 12)) (q37 (_ BitVec 12)) (q38 (_ BitVec 12)) (q39 (_ BitVec 12)) (q40 (_ BitVec 12)) (q41 (_ BitVec 12)) (q42 (_ BitVec 12)) (q43 (_ BitVec 12)) (q44 (_ BitVec 12)) (q45 (_ BitVec 12)) (q46 (_ BitVec 12)) (q47 (_ BitVec 12)) (q48 (_ BitVec 12)) (q49 (_ BitVec 12)) (q50 (_ BitVec 12)) (q51 (_ BitVec 12)) (q52 (_ BitVec 12)) (q53 (_ BitVec 9))) (=> (distinct (bvlshr q51 q44) q35) (= (bvsub (bvnot q53) (bvnot q53)) q53))))
(assert (forall ((q54 (_ BitVec 12)) (q55 (_ BitVec 12)) (q56 (_ BitVec 12)) (q57 (_ BitVec 12)) (q58 (_ BitVec 12)) (q59 (_ BitVec 9))) (=> (= q54 q54) (bvult (bvsub (bvshl q59 (bvnot q59)) (bvnot q59)) (bvsub (bvshl q59 (bvnot q59)) (bvnot q59))))))
(assert (forall ((q64 (_ BitVec 12)) (q65 (_ BitVec 12)) (q66 (_ BitVec 8))) (=> (distinct (bvashr q66 q66) q66) (= (bvneg q65) (bvashr q65 (bvneg q65))))))
(assert (forall ((q67 (_ BitVec 12)) (q68 (_ BitVec 12)) (q69 (_ BitVec 12)) (q70 (_ BitVec 12)) (q71 (_ BitVec 12)) (q72 (_ BitVec 12)) (q73 (_ BitVec 12)) (q74 (_ BitVec 12)) (q75 (_ BitVec 12)) (q76 (_ BitVec 12)) (q77 (_ BitVec 12)) (q78 (_ BitVec 12)) (q79 (_ BitVec 12)) (q80 (_ BitVec 12)) (q81 (_ BitVec 12)) (q82 (_ BitVec 12)) (q83 (_ BitVec 12)) (q84 (_ BitVec 12)) (q85 (_ BitVec 12)) (q86 (_ BitVec 12)) (q87 (_ BitVec 12)) (q88 (_ BitVec 14))) (=> (= (bvsmod q88 q88) (bvsmod q88 q88)) (distinct q73 q69))))
(assert (forall ((q107 (_ BitVec 12)) (q108 (_ BitVec 12)) (q109 (_ BitVec 12)) (q110 (_ BitVec 12)) (q111 (_ BitVec 12)) (q112 (_ BitVec 8))) (=> (= q112 (bvlshr q112 q112)) (= q108 q109))))
(assert (forall ((q122 (_ BitVec 12)) (q123 (_ BitVec 12)) (q124 (_ BitVec 12)) (q125 (_ BitVec 12)) (q126 (_ BitVec 12)) (q127 (_ BitVec 12)) (q128 (_ BitVec 12)) (q129 (_ BitVec 12)) (q130 (_ BitVec 12)) (q131 (_ BitVec 12)) (q132 (_ BitVec 12)) (q133 (_ BitVec 11))) (=> (distinct (bvnor q133 q133) (bvurem (bvnor q133 q133) q133)) (distinct q127 q125))))
(assert (forall ((q134 (_ BitVec 12)) (q135 (_ BitVec 12)) (q136 (_ BitVec 12)) (q137 (_ BitVec 8))) (=> (bvsle (bvnot q135) q136) (bvule (bvsdiv (bvnor q137 q137) q137) (bvashr (bvsdiv (bvnor q137 q137) q137) (bvsmod (bvnor q137 q137) q137))))))
(check-sat)

 Exception in thread "main" java.lang.AssertionError: assertion failed                                                                                                                              [6/1977]
        at scala.Predef$.assert(Predef.scala:156)
        at lazabs.horn.bottomup.HornWrapper$.verifyCEX(HornWrapper.scala:91)
        at lazabs.horn.bottomup.InnerHornWrapper.<init>(HornWrapper.scala:390)
        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)

'-assert', '-abstract:relEqs'

(declare-datatypes ((C_dtp 0)) (((cons_c (n Int)))))
(declare-datatypes ((B_dtp 0)) (((cons_b (elem C_dtp)))))

(assert
  (=
    (_size (cons_b (cons_c 0)))
    2
  )
)

(check-sat)

 Exception in thread "main" java.lang.AssertionError: assertion failed                                                                                                                            [121/1865]
        at scala.Predef$.assert(Predef.scala:156)
        at ap.basetypes.IdealInt.getHighestSetBit(IdealInt.scala:664)
        at ap.theories.bitvectors.ModReducer$Reducer$$anonfun$reduce$1$$anonfun$2.apply(ModReducer.scala:320)
        at ap.theories.bitvectors.ModReducer$Reducer$$anonfun$reduce$1$$anonfun$2.apply(ModReducer.scala:316)
        at ap.util.LRUCache.apply(LRUCache.scala:37)
        at ap.theories.bitvectors.ModReducer$Reducer$$anonfun$reduce$1.apply(ModReducer.scala:315)
        at ap.theories.bitvectors.ModReducer$Reducer$$anonfun$reduce$1.apply(ModReducer.scala:185)
        at ap.terfor.conjunctions.ReducerPlugin$.rewritePreds(ReducerPlugin.scala:89)
        at ap.theories.bitvectors.ModReducer$Reducer.reduce(ModReducer.scala:185)
        at ap.terfor.conjunctions.SeqReducerPlugin.reduce(ReducerPlugin.scala:371)
        at ap.terfor.conjunctions.ReduceWithConjunction.ap$terfor$conjunctions$ReduceWithConjunction$$reduceWithPlugin(ReduceWithConjunction.scala:621)
        at ap.terfor.conjunctions.ReduceWithConjunction$.ap$terfor$conjunctions$ReduceWithConjunction$$reduceConj(ReduceWithConjunction.scala:91)
...

'-assert', '-noSlicing', '-abstract:relIneqs'

(assert true)

(assert (not (exists ()false)))

Error in conversion from Princess to Eldarica (ITerm): bv_extract(0, 0, P10) sublcass of class ap.parser.IFunApp

$ time eld -horn -abstract:off -cex has_cex.smt2
unsat
<entire_cex>
eld -horn -abstract:off -cex has_cex.smt2  96.14s user 1.17s system 195% cpu 49.832 total

$ time eld -horn -abstract:off -t:300 -cex has_cex.smt2

(declare-datatypes ((MList 0)) (((mcons  (mhead Int) (mtail MList)) (mnill))))
(declare-fun x () MList)
(declare-fun y () MList)
(assert (and ((_ is mcons) x) (= (mtail x) y) (= y mnill))) ;;valid according to smtlib but Eldarica does not accept this
;; (assert (and (is-mcons x) (= (mtail x) y) (= y mnill))) ;;ALL smt solvers accept this recognizer
(check-sat)

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

 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)

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

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)

(declare-fun p ((Array Int Bool)) Bool)

(assert
  (p
    (store ((as const (Array Int Bool)) false) 1 3)
  )
)

$ ~/eldarica/eld -assert  test.smt2 
sat

Exception in thread "main" java.lang.RuntimeException: java.lang.UnsupportedOperationException: empty.head
    at jayhorn.checker.Checker.checkProgram(Checker.java:818)
    at jayhorn.Main.main(Main.java:71)
Caused by: java.lang.UnsupportedOperationException: empty.head
    at scala.collection.immutable.Vector.head(Vector.scala:193)
    at lazabs.horn.bottomup.DisjInterpolator$$anonfun$lazabs$horn$bottomup$DisjInterpolator$$predicateGeneratorHelp$1.lazabs$horn$bottomup$DisjInterpolator$$anonfun$$refine$1(DisjInterpolator.scala:438)
    at lazabs.horn.bottomup.DisjInterpolator$$anonfun$lazabs$horn$bottomup$DisjInterpolator$$predicateGeneratorHelp$1$$anonfun$16.apply(DisjInterpolator.scala:459)
    at lazabs.horn.bottomup.DisjInterpolator$$anonfun$lazabs$horn$bottomup$DisjInterpolator$$predicateGeneratorHelp$1$$anonfun$16.apply(DisjInterpolator.scala:459)
    at scala.collection.immutable.List.map(List.scala:273)
    at lazabs.horn.bottomup.DisjInterpolator$$anonfun$lazabs$horn$bottomup$DisjInterpolator$$predicateGeneratorHelp$1.lazabs$horn$bottomup$DisjInterpolator$$anonfun$$refine$1(DisjInterpolator.scala:459)
    at lazabs.horn.bottomup.DisjInterpolator$$anonfun$lazabs$horn$bottomup$DisjInterpolator$$predicateGeneratorHelp$1$$anonfun$15.apply(DisjInterpolator.scala:449)
    at lazabs.horn.bottomup.DisjInterpolator$$anonfun$lazabs$horn$bottomup$DisjInterpolator$$predicateGeneratorHelp$1$$anonfun$15.apply(DisjInterpolator.scala:449)
    at scala.collection.TraversableLike$WithFilter$$anonfun$map$2.apply(TraversableLike.scala:728)
    at scala.collection.immutable.List.foreach(List.scala:381)
    at scala.collection.TraversableLike$WithFilter.map(TraversableLike.scala:727)
    at lazabs.horn.bottomup.DisjInterpolator$$anonfun$lazabs$horn$bottomup$DisjInterpolator$$predicateGeneratorHelp$1.lazabs$horn$bottomup$DisjInterpolator$$anonfun$$refine$1(DisjInterpolator.scala:449)
    at lazabs.horn.bottomup.DisjInterpolator$$anonfun$lazabs$horn$bottomup$DisjInterpolator$$predicateGeneratorHelp$1$$anonfun$16.apply(DisjInterpolator.scala:459)
    at lazabs.horn.bottomup.DisjInterpolator$$anonfun$lazabs$horn$bottomup$DisjInterpolator$$predicateGeneratorHelp$1$$anonfun$16.apply(DisjInterpolator.scala:459)
    at scala.collection.immutable.List.map(List.scala:277)
    at lazabs.horn.bottomup.DisjInterpolator$$anonfun$lazabs$horn$bottomup$DisjInterpolator$$predicateGeneratorHelp$1.lazabs$horn$bottomup$DisjInterpolator$$anonfun$$refine$1(DisjInterpolator.scala:459)
    at lazabs.horn.bottomup.DisjInterpolator$$anonfun$lazabs$horn$bottomup$DisjInterpolator$$predicateGeneratorHelp$1$$anonfun$15.apply(DisjInterpolator.scala:449)
    at lazabs.horn.bottomup.DisjInterpolator$$anonfun$lazabs$horn$bottomup$DisjInterpolator$$predicateGeneratorHelp$1$$anonfun$15.apply(DisjInterpolator.scala:449)
    at scala.collection.TraversableLike$WithFilter$$anonfun$map$2.apply(TraversableLike.scala:728)
    at scala.collection.immutable.List.foreach(List.scala:381)
    at scala.collection.TraversableLike$WithFilter.map(TraversableLike.scala:727)
    at lazabs.horn.bottomup.DisjInterpolator$$anonfun$lazabs$horn$bottomup$DisjInterpolator$$predicateGeneratorHelp$1.lazabs$horn$bottomup$DisjInterpolator$$anonfun$$refine$1(DisjInterpolator.scala:449)
    at lazabs.horn.bottomup.DisjInterpolator$$anonfun$lazabs$horn$bottomup$DisjInterpolator$$predicateGeneratorHelp$1$$anonfun$16.apply(DisjInterpolator.scala:459)
    at lazabs.horn.bottomup.DisjInterpolator$$anonfun$lazabs$horn$bottomup$DisjInterpolator$$predicateGeneratorHelp$1$$anonfun$16.apply(DisjInterpolator.scala:459)
    at scala.collection.immutable.List.map(List.scala:273)
    at lazabs.horn.bottomup.DisjInterpolator$$anonfun$lazabs$horn$bottomup$DisjInterpolator$$predicateGeneratorHelp$1.lazabs$horn$bottomup$DisjInterpolator$$anonfun$$refine$1(DisjInterpolator.scala:459)
    at lazabs.horn.bottomup.DisjInterpolator$$anonfun$lazabs$horn$bottomup$DisjInterpolator$$predicateGeneratorHelp$1$$anonfun$15.apply(DisjInterpolator.scala:449)
    at lazabs.horn.bottomup.DisjInterpolator$$anonfun$lazabs$horn$bottomup$DisjInterpolator$$predicateGeneratorHelp$1$$anonfun$15.apply(DisjInterpolator.scala:449)
    at scala.collection.TraversableLike$WithFilter$$anonfun$map$2.apply(TraversableLike.scala:728)
    at scala.collection.immutable.List.foreach(List.scala:381)
    at scala.collection.TraversableLike$WithFilter.map(TraversableLike.scala:727)
    at lazabs.horn.bottomup.DisjInterpolator$$anonfun$lazabs$horn$bottomup$DisjInterpolator$$predicateGeneratorHelp$1.lazabs$horn$bottomup$DisjInterpolator$$anonfun$$refine$1(DisjInterpolator.scala:449)
    at lazabs.horn.bottomup.DisjInterpolator$$anonfun$lazabs$horn$bottomup$DisjInterpolator$$predicateGeneratorHelp$1$$anonfun$16.apply(DisjInterpolator.scala:459)
    at lazabs.horn.bottomup.DisjInterpolator$$anonfun$lazabs$horn$bottomup$DisjInterpolator$$predicateGeneratorHelp$1$$anonfun$16.apply(DisjInterpolator.scala:459)
    at scala.collection.immutable.List.map(List.scala:277)
    at lazabs.horn.bottomup.DisjInterpolator$$anonfun$lazabs$horn$bottomup$DisjInterpolator$$predicateGeneratorHelp$1.lazabs$horn$bottomup$DisjInterpolator$$anonfun$$refine$1(DisjInterpolator.scala:459)
    at lazabs.horn.bottomup.DisjInterpolator$$anonfun$lazabs$horn$bottomup$DisjInterpolator$$predicateGeneratorHelp$1$$anonfun$15.apply(DisjInterpolator.scala:449)
    at lazabs.horn.bottomup.DisjInterpolator$$anonfun$lazabs$horn$bottomup$DisjInterpolator$$predicateGeneratorHelp$1$$anonfun$15.apply(DisjInterpolator.scala:449)
    at scala.collection.TraversableLike$WithFilter$$anonfun$map$2.apply(TraversableLike.scala:728)
    at scala.collection.immutable.List.foreach(List.scala:381)
    at scala.collection.TraversableLike$WithFilter.map(TraversableLike.scala:727)
    at lazabs.horn.bottomup.DisjInterpolator$$anonfun$lazabs$horn$bottomup$DisjInterpolator$$predicateGeneratorHelp$1.lazabs$horn$bottomup$DisjInterpolator$$anonfun$$refine$1(DisjInterpolator.scala:449)
    at lazabs.horn.bottomup.DisjInterpolator$$anonfun$lazabs$horn$bottomup$DisjInterpolator$$predicateGeneratorHelp$1$$anonfun$16.apply(DisjInterpolator.scala:459)
    at lazabs.horn.bottomup.DisjInterpolator$$anonfun$lazabs$horn$bottomup$DisjInterpolator$$predicateGeneratorHelp$1$$anonfun$16.apply(DisjInterpolator.scala:459)
    at scala.collection.immutable.List.map(List.scala:273)
    at lazabs.horn.bottomup.DisjInterpolator$$anonfun$lazabs$horn$bottomup$DisjInterpolator$$predicateGeneratorHelp$1.lazabs$horn$bottomup$DisjInterpolator$$anonfun$$refine$1(DisjInterpolator.scala:459)
    at lazabs.horn.bottomup.DisjInterpolator$$anonfun$lazabs$horn$bottomup$DisjInterpolator$$predicateGeneratorHelp$1$$anonfun$15.apply(DisjInterpolator.scala:449)
    at lazabs.horn.bottomup.DisjInterpolator$$anonfun$lazabs$horn$bottomup$DisjInterpolator$$predicateGeneratorHelp$1$$anonfun$15.apply(DisjInterpolator.scala:449)
    at scala.collection.TraversableLike$WithFilter$$anonfun$map$2.apply(TraversableLike.scala:728)
    at scala.collection.immutable.List.foreach(List.scala:381)
    at scala.collection.TraversableLike$WithFilter.map(TraversableLike.scala:727)
    at lazabs.horn.bottomup.DisjInterpolator$$anonfun$lazabs$horn$bottomup$DisjInterpolator$$predicateGeneratorHelp$1.lazabs$horn$bottomup$DisjInterpolator$$anonfun$$refine$1(DisjInterpolator.scala:449)
    at lazabs.horn.bottomup.DisjInterpolator$$anonfun$lazabs$horn$bottomup$DisjInterpolator$$predicateGeneratorHelp$1$$anonfun$16.apply(DisjInterpolator.scala:459)
    at lazabs.horn.bottomup.DisjInterpolator$$anonfun$lazabs$horn$bottomup$DisjInterpolator$$predicateGeneratorHelp$1$$anonfun$16.apply(DisjInterpolator.scala:459)
    at scala.collection.immutable.List.map(List.scala:273)
    at lazabs.horn.bottomup.DisjInterpolator$$anonfun$lazabs$horn$bottomup$DisjInterpolator$$predicateGeneratorHelp$1.lazabs$horn$bottomup$DisjInterpolator$$anonfun$$refine$1(DisjInterpolator.scala:459)
    at lazabs.horn.bottomup.DisjInterpolator$$anonfun$lazabs$horn$bottomup$DisjInterpolator$$predicateGeneratorHelp$1$$anonfun$15.apply(DisjInterpolator.scala:449)
    at lazabs.horn.bottomup.DisjInterpolator$$anonfun$lazabs$horn$bottomup$DisjInterpolator$$predicateGeneratorHelp$1$$anonfun$15.apply(DisjInterpolator.scala:449)
    at scala.collection.TraversableLike$WithFilter$$anonfun$map$2.apply(TraversableLike.scala:728)
    at scala.collection.immutable.List.foreach(List.scala:381)
    at scala.collection.TraversableLike$WithFilter.map(TraversableLike.scala:727)
    at lazabs.horn.bottomup.DisjInterpolator$$anonfun$lazabs$horn$bottomup$DisjInterpolator$$predicateGeneratorHelp$1.lazabs$horn$bottomup$DisjInterpolator$$anonfun$$refine$1(DisjInterpolator.scala:449)
    at lazabs.horn.bottomup.DisjInterpolator$$anonfun$lazabs$horn$bottomup$DisjInterpolator$$predicateGeneratorHelp$1$$anonfun$16.apply(DisjInterpolator.scala:459)
    at lazabs.horn.bottomup.DisjInterpolator$$anonfun$lazabs$horn$bottomup$DisjInterpolator$$predicateGeneratorHelp$1$$anonfun$16.apply(DisjInterpolator.scala:459)
    at scala.collection.immutable.List.map(List.scala:273)
    at lazabs.horn.bottomup.DisjInterpolator$$anonfun$lazabs$horn$bottomup$DisjInterpolator$$predicateGeneratorHelp$1.lazabs$horn$bottomup$DisjInterpolator$$anonfun$$refine$1(DisjInterpolator.scala:459)
    at lazabs.horn.bottomup.DisjInterpolator$$anonfun$lazabs$horn$bottomup$DisjInterpolator$$predicateGeneratorHelp$1$$anonfun$15.apply(DisjInterpolator.scala:449)
    at lazabs.horn.bottomup.DisjInterpolator$$anonfun$lazabs$horn$bottomup$DisjInterpolator$$predicateGeneratorHelp$1$$anonfun$15.apply(DisjInterpolator.scala:449)
    at scala.collection.TraversableLike$WithFilter$$anonfun$map$2.apply(TraversableLike.scala:728)
    at scala.collection.immutable.List.foreach(List.scala:381)
    at scala.collection.TraversableLike$WithFilter.map(TraversableLike.scala:727)
    at lazabs.horn.bottomup.DisjInterpolator$$anonfun$lazabs$horn$bottomup$DisjInterpolator$$predicateGeneratorHelp$1.lazabs$horn$bottomup$DisjInterpolator$$anonfun$$refine$1(DisjInterpolator.scala:449)
    at lazabs.horn.bottomup.DisjInterpolator$$anonfun$lazabs$horn$bottomup$DisjInterpolator$$predicateGeneratorHelp$1$$anonfun$16.apply(DisjInterpolator.scala:459)
    at lazabs.horn.bottomup.DisjInterpolator$$anonfun$lazabs$horn$bottomup$DisjInterpolator$$predicateGeneratorHelp$1$$anonfun$16.apply(DisjInterpolator.scala:459)
    at scala.collection.immutable.List.map(List.scala:273)
    at lazabs.horn.bottomup.DisjInterpolator$$anonfun$lazabs$horn$bottomup$DisjInterpolator$$predicateGeneratorHelp$1.lazabs$horn$bottomup$DisjInterpolator$$anonfun$$refine$1(DisjInterpolator.scala:459)
    at lazabs.horn.bottomup.DisjInterpolator$$anonfun$lazabs$horn$bottomup$DisjInterpolator$$predicateGeneratorHelp$1$$anonfun$15.apply(DisjInterpolator.scala:449)
    at lazabs.horn.bottomup.DisjInterpolator$$anonfun$lazabs$horn$bottomup$DisjInterpolator$$predicateGeneratorHelp$1$$anonfun$15.apply(DisjInterpolator.scala:449)
    at scala.collection.TraversableLike$WithFilter$$anonfun$map$2.apply(TraversableLike.scala:728)
    at scala.collection.immutable.List.foreach(List.scala:381)
    at scala.collection.TraversableLike$WithFilter.map(TraversableLike.scala:727)
    at lazabs.horn.bottomup.DisjInterpolator$$anonfun$lazabs$horn$bottomup$DisjInterpolator$$predicateGeneratorHelp$1.lazabs$horn$bottomup$DisjInterpolator$$anonfun$$refine$1(DisjInterpolator.scala:449)
    at lazabs.horn.bottomup.DisjInterpolator$$anonfun$lazabs$horn$bottomup$DisjInterpolator$$predicateGeneratorHelp$1$$anonfun$16.apply(DisjInterpolator.scala:459)
    at lazabs.horn.bottomup.DisjInterpolator$$anonfun$lazabs$horn$bottomup$DisjInterpolator$$predicateGeneratorHelp$1$$anonfun$16.apply(DisjInterpolator.scala:459)
    at scala.collection.immutable.List.map(List.scala:273)
    at lazabs.horn.bottomup.DisjInterpolator$$anonfun$lazabs$horn$bottomup$DisjInterpolator$$predicateGeneratorHelp$1.lazabs$horn$bottomup$DisjInterpolator$$anonfun$$refine$1(DisjInterpolator.scala:459)
    at lazabs.horn.bottomup.DisjInterpolator$$anonfun$lazabs$horn$bottomup$DisjInterpolator$$predicateGeneratorHelp$1$$anonfun$15.apply(DisjInterpolator.scala:449)
    at lazabs.horn.bottomup.DisjInterpolator$$anonfun$lazabs$horn$bottomup$DisjInterpolator$$predicateGeneratorHelp$1$$anonfun$15.apply(DisjInterpolator.scala:449)
    at scala.collection.TraversableLike$WithFilter$$anonfun$map$2.apply(TraversableLike.scala:728)
    at scala.collection.immutable.List.foreach(List.scala:381)
    at scala.collection.TraversableLike$WithFilter.map(TraversableLike.scala:727)
    at lazabs.horn.bottomup.DisjInterpolator$$anonfun$lazabs$horn$bottomup$DisjInterpolator$$predicateGeneratorHelp$1.lazabs$horn$bottomup$DisjInterpolator$$anonfun$$refine$1(DisjInterpolator.scala:449)
    at lazabs.horn.bottomup.DisjInterpolator$$anonfun$lazabs$horn$bottomup$DisjInterpolator$$predicateGeneratorHelp$1$$anonfun$16.apply(DisjInterpolator.scala:459)
    at lazabs.horn.bottomup.DisjInterpolator$$anonfun$lazabs$horn$bottomup$DisjInterpolator$$predicateGeneratorHelp$1$$anonfun$16.apply(DisjInterpolator.scala:459)
    at scala.collection.immutable.List.map(List.scala:273)
    at lazabs.horn.bottomup.DisjInterpolator$$anonfun$lazabs$horn$bottomup$DisjInterpolator$$predicateGeneratorHelp$1.lazabs$horn$bottomup$DisjInterpolator$$anonfun$$refine$1(DisjInterpolator.scala:459)
    at lazabs.horn.bottomup.DisjInterpolator$$anonfun$lazabs$horn$bottomup$DisjInterpolator$$predicateGeneratorHelp$1$$anonfun$15.apply(DisjInterpolator.scala:449)
    at lazabs.horn.bottomup.DisjInterpolator$$anonfun$lazabs$horn$bottomup$DisjInterpolator$$predicateGeneratorHelp$1$$anonfun$15.apply(DisjInterpolator.scala:449)
    at scala.collection.TraversableLike$WithFilter$$anonfun$map$2.apply(TraversableLike.scala:728)
    at scala.collection.immutable.List.foreach(List.scala:381)
    at scala.collection.TraversableLike$WithFilter.map(TraversableLike.scala:727)
    at lazabs.horn.bottomup.DisjInterpolator$$anonfun$lazabs$horn$bottomup$DisjInterpolator$$predicateGeneratorHelp$1.lazabs$horn$bottomup$DisjInterpolator$$anonfun$$refine$1(DisjInterpolator.scala:449)
    at lazabs.horn.bottomup.DisjInterpolator$$anonfun$lazabs$horn$bottomup$DisjInterpolator$$predicateGeneratorHelp$1$$anonfun$16.apply(DisjInterpolator.scala:459)
    at lazabs.horn.bottomup.DisjInterpolator$$anonfun$lazabs$horn$bottomup$DisjInterpolator$$predicateGeneratorHelp$1$$anonfun$16.apply(DisjInterpolator.scala:459)
    at scala.collection.immutable.List.map(List.scala:273)
    at lazabs.horn.bottomup.DisjInterpolator$$anonfun$lazabs$horn$bottomup$DisjInterpolator$$predicateGeneratorHelp$1.lazabs$horn$bottomup$DisjInterpolator$$anonfun$$refine$1(DisjInterpolator.scala:459)
    at lazabs.horn.bottomup.DisjInterpolator$$anonfun$lazabs$horn$bottomup$DisjInterpolator$$predicateGeneratorHelp$1$$anonfun$15.apply(DisjInterpolator.scala:449)
    at lazabs.horn.bottomup.DisjInterpolator$$anonfun$lazabs$horn$bottomup$DisjInterpolator$$predicateGeneratorHelp$1$$anonfun$15.apply(DisjInterpolator.scala:449)
    at scala.collection.TraversableLike$WithFilter$$anonfun$map$2.apply(TraversableLike.scala:728)
    at scala.collection.immutable.List.foreach(List.scala:381)
    at scala.collection.TraversableLike$WithFilter.map(TraversableLike.scala:727)
    at lazabs.horn.bottomup.DisjInterpolator$$anonfun$lazabs$horn$bottomup$DisjInterpolator$$predicateGeneratorHelp$1.lazabs$horn$bottomup$DisjInterpolator$$anonfun$$refine$1(DisjInterpolator.scala:449)
    at lazabs.horn.bottomup.DisjInterpolator$$anonfun$lazabs$horn$bottomup$DisjInterpolator$$predicateGeneratorHelp$1$$anonfun$16.apply(DisjInterpolator.scala:459)
    at lazabs.horn.bottomup.DisjInterpolator$$anonfun$lazabs$horn$bottomup$DisjInterpolator$$predicateGeneratorHelp$1$$anonfun$16.apply(DisjInterpolator.scala:459)
    at scala.collection.immutable.List.map(List.scala:273)
    at lazabs.horn.bottomup.DisjInterpolator$$anonfun$lazabs$horn$bottomup$DisjInterpolator$$predicateGeneratorHelp$1.lazabs$horn$bottomup$DisjInterpolator$$anonfun$$refine$1(DisjInterpolator.scala:459)
    at lazabs.horn.bottomup.DisjInterpolator$$anonfun$lazabs$horn$bottomup$DisjInterpolator$$predicateGeneratorHelp$1$$anonfun$15.apply(DisjInterpolator.scala:449)
    at lazabs.horn.bottomup.DisjInterpolator$$anonfun$lazabs$horn$bottomup$DisjInterpolator$$predicateGeneratorHelp$1$$anonfun$15.apply(DisjInterpolator.scala:449)
    at scala.collection.TraversableLike$WithFilter$$anonfun$map$2.apply(TraversableLike.scala:728)
    at scala.collection.immutable.List.foreach(List.scala:381)
    at scala.collection.TraversableLike$WithFilter.map(TraversableLike.scala:727)
    at lazabs.horn.bottomup.DisjInterpolator$$anonfun$lazabs$horn$bottomup$DisjInterpolator$$predicateGeneratorHelp$1.lazabs$horn$bottomup$DisjInterpolator$$anonfun$$refine$1(DisjInterpolator.scala:449)
    at lazabs.horn.bottomup.DisjInterpolator$$anonfun$lazabs$horn$bottomup$DisjInterpolator$$predicateGeneratorHelp$1$$anonfun$16.apply(DisjInterpolator.scala:459)
    at lazabs.horn.bottomup.DisjInterpolator$$anonfun$lazabs$horn$bottomup$DisjInterpolator$$predicateGeneratorHelp$1$$anonfun$16.apply(DisjInterpolator.scala:459)
    at scala.collection.immutable.List.map(List.scala:273)
    at lazabs.horn.bottomup.DisjInterpolator$$anonfun$lazabs$horn$bottomup$DisjInterpolator$$predicateGeneratorHelp$1.lazabs$horn$bottomup$DisjInterpolator$$anonfun$$refine$1(DisjInterpolator.scala:459)
    at lazabs.horn.bottomup.DisjInterpolator$$anonfun$lazabs$horn$bottomup$DisjInterpolator$$predicateGeneratorHelp$1$$anonfun$15.apply(DisjInterpolator.scala:449)
    at lazabs.horn.bottomup.DisjInterpolator$$anonfun$lazabs$horn$bottomup$DisjInterpolator$$predicateGeneratorHelp$1$$anonfun$15.apply(DisjInterpolator.scala:449)
    at scala.collection.TraversableLike$WithFilter$$anonfun$map$2.apply(TraversableLike.scala:728)
    at scala.collection.immutable.List.foreach(List.scala:381)
    at scala.collection.TraversableLike$WithFilter.map(TraversableLike.scala:727)
    at lazabs.horn.bottomup.DisjInterpolator$$anonfun$lazabs$horn$bottomup$DisjInterpolator$$predicateGeneratorHelp$1.lazabs$horn$bottomup$DisjInterpolator$$anonfun$$refine$1(DisjInterpolator.scala:449)
    at lazabs.horn.bottomup.DisjInterpolator$$anonfun$lazabs$horn$bottomup$DisjInterpolator$$predicateGeneratorHelp$1.apply(DisjInterpolator.scala:499)
    at lazabs.horn.bottomup.DisjInterpolator$$anonfun$lazabs$horn$bottomup$DisjInterpolator$$predicateGeneratorHelp$1.apply(DisjInterpolator.scala:194)
    at ap.SimpleAPI$.withProver(SimpleAPI.scala:128)
    at lazabs.horn.bottomup.DisjInterpolator$.lazabs$horn$bottomup$DisjInterpolator$$predicateGeneratorHelp(DisjInterpolator.scala:194)
    at lazabs.horn.bottomup.DisjInterpolator$$anonfun$predicateGenerator$1.apply$mcV$sp(DisjInterpolator.scala:138)
    at lazabs.horn.bottomup.DisjInterpolator$$anonfun$predicateGenerator$1.apply(DisjInterpolator.scala:138)
    at lazabs.horn.bottomup.DisjInterpolator$$anonfun$predicateGenerator$1.apply(DisjInterpolator.scala:138)
    at scala.util.DynamicVariable.withValue(DynamicVariable.scala:58)
    at ap.util.Timeout$.withChecker(Timeout.scala:44)
    at ap.util.Timeout$$anonfun$withTimeoutMillis$1.apply(Timeout.scala:58)
    at ap.util.Timeout$.catchTimeout(Timeout.scala:88)
    at ap.util.Timeout$.withTimeoutMillis(Timeout.scala:61)
    at lazabs.horn.bottomup.DisjInterpolator$.predicateGenerator(DisjInterpolator.scala:155)
    at lazabs.horn.bottomup.DagInterpolator$.interpolatingPredicateGenCEXAndOr(DagInterpolator.scala:156)
    at lazabs.horn.bottomup.SimpleWrapper$$anonfun$solve$1$$anonfun$apply$1$$anonfun$2.apply(SimpleWrapper.scala:69)
    at lazabs.horn.bottomup.SimpleWrapper$$anonfun$solve$1$$anonfun$apply$1$$anonfun$2.apply(SimpleWrapper.scala:69)
    at lazabs.horn.bottomup.HornPredAbs.liftedTree1$1(HornPredAbs.scala:937)
    at lazabs.horn.bottomup.HornPredAbs.<init>(HornPredAbs.scala:917)
    at lazabs.horn.bottomup.SimpleWrapper$$anonfun$solve$1$$anonfun$apply$1.apply(SimpleWrapper.scala:73)
    at lazabs.horn.bottomup.SimpleWrapper$$anonfun$solve$1$$anonfun$apply$1.apply(SimpleWrapper.scala:51)
    at scala.util.DynamicVariable.withValue(DynamicVariable.scala:58)
    at scala.Console$.withOut(Console.scala:53)
    at lazabs.horn.bottomup.SimpleWrapper$$anonfun$solve$1.apply(SimpleWrapper.scala:51)
    at lazabs.horn.bottomup.SimpleWrapper$$anonfun$solve$1.apply(SimpleWrapper.scala:51)
    at scala.util.DynamicVariable.withValue(DynamicVariable.scala:58)
    at scala.Console$.withErr(Console.scala:92)
    at lazabs.horn.bottomup.SimpleWrapper$.solve(SimpleWrapper.scala:51)
    at lazabs.horn.bottomup.SimpleWrapper.solve(SimpleWrapper.scala)
    at jayhorn.solver.princess.PrincessProver.checkSat(PrincessProver.java:334)
    at jayhorn.checker.Checker.checkProgram(Checker.java:811)
    ... 1 more

(set-logic HORN)
(assert (forall ((q0 (_ BitVec 9)) (q1 (_ BitVec 12))) (=> (distinct q0 q0) (bvslt (bvsmod q1 q1) q1))))
(assert (forall ((q3 (_ BitVec 9)) (q4 (_ BitVec 9)) (q5 (_ BitVec 8))) (=> (bvule q4 (bvnor q3 q3)) (distinct (bvlshr (bvsdiv q5 q5) (bvsdiv q5 q5)) (bvsdiv q5 q5)))))
(check-sat)

Theories: GroebnerMultiplication, ModuloArithmetic
WARNING: unbounded shift r_shift_cast(0, 255, all_3_2 + -256*sc_39_0_0, all_6_3 + -256*sc_30_0_0, all_6_0)
WARNING: unbounded shift r_shift_cast(0, 255, all_3_2 + -256*sc_39_0_0, all_6_3 + -256*sc_30_0_0, all_6_0)
WARNING: unbounded shift r_shift_cast(0, 255, all_3_2 + -256*sc_39_0_0, all_6_3 + -256*sc_30_0_0, all_6_0)
WARNING: unbounded shift r_shift_cast(0, 255, all_3_2 + -256*sc_39_0_0, all_6_3 + -256*sc_30_0_0, all_6_0)
WARNING: unbounded shift r_shift_cast(0, 255, all_3_2 + -256*sc_39_0_0, all_6_3 + -256*sc_30_0_0, all_6_0)
WARNING: unbounded shift r_shift_cast(0, 255, all_3_2 + -256*sc_39_0_0, all_6_3 + -256*sc_30_0_0, all_6_0)
WARNING: unbounded shift r_shift_cast(0, 255, all_3_2 + -256*sc_39_0_0, all_6_3 + -256*sc_30_0_0, all_6_0)
WARNING: unbounded shift r_shift_cast(0, 255, all_3_2 + -256*sc_39_0_0, all_6_3 + -256*sc_30_0_0, all_6_0)
WARNING: unbounded shift r_shift_cast(0, 255, all_3_2 + -256*sc_39_0_0, all_6_3 + -256*sc_30_0_0, all_6_0)
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:433)
        at lazabs.horn.bottomup.HornWrapper$$anonfun$11.apply(HornWrapper.scala:254)
        at lazabs.horn.bottomup.HornWrapper$$anonfun$11.apply(HornWrapper.scala:256)
        at lazabs.ParallelComputation$.apply(ParallelComputation.scala:46)
        at lazabs.horn.bottomup.HornWrapper.<init>(HornWrapper.scala:253)
        at lazabs.horn.Solve$.apply(Solve.scala:81)
        at lazabs.Main$.doMain(Main.scala:601)
        at lazabs.Main$.main(Main.scala:271)
        at lazabs.Main.main(Main.scala)

Theories: GroebnerMultiplication
Exception in thread "main" java.lang.AssertionError: assertion failed
        at scala.Predef$.assert(Predef.scala:156)
        at ap.theories.nia.Basis.add(Polynomial.scala:771)
        at ap.theories.nia.Basis.simplify(Polynomial.scala:940)
        at ap.theories.nia.GroebnerMultiplication$$anon$1$$anonfun$4.apply(GroebnerMultiplication.scala:362)
        at ap.theories.nia.GroebnerMultiplication$$anon$1$$anonfun$4.apply(GroebnerMultiplication.scala:345)
        at ap.util.LRUCache.apply(LRUCache.scala:37)
        at ap.theories.nia.GroebnerMultiplication$$anon$1.ap$theories$nia$GroebnerMultiplication$$anon$$handleGoalAux(GroebnerMultiplication.scala:345)
        at ap.theories.nia.GroebnerMultiplication$$anon$1.handleGoal(GroebnerMultiplication.scala:212)
        at ap.proof.theoryPlugins.PluginTask.apply(Plugin.scala:392)
        at ap.proof.goal.Goal.step(Goal.scala:395)
        at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:470)
        at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:530)
        at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:476)
        at ap.proof.ModelSearchProver$IncProverImpl.checkValidityDir(ModelSearchProver.scala:1079)
        at ap.proof.ModelSearchProver$IncProverImpl.checkValidityDir(ModelSearchProver.scala:1069)
        at ap.proof.ModelSearchProver$IncProverImpl.checkValidity(ModelSearchProver.scala:1057)
        at lazabs.horn.bottomup.HornPredAbs$$anonfun$isValid$1.apply$mcZ$sp(HornPredAbs.scala:703)
        at lazabs.horn.bottomup.HornPredAbs$$anonfun$isValid$1.apply(HornPredAbs.scala:694)
        at lazabs.horn.bottomup.HornPredAbs$$anonfun$isValid$1.apply(HornPredAbs.scala:694)
        at scala.util.DynamicVariable.withValue(DynamicVariable.scala:58)
        at ap.util.Timeout$.withChecker(Timeout.scala:44)
        at lazabs.horn.bottomup.HornPredAbs.isValid(HornPredAbs.scala:694)
        at lazabs.horn.bottomup.HornPredAbs$$anonfun$genEdge$1.apply(HornPredAbs.scala:1430)
        at lazabs.horn.bottomup.HornPredAbs$$anonfun$genEdge$1.apply(HornPredAbs.scala:1421)
        at lazabs.horn.bottomup.Hasher.scope(Hasher.scala:356)
        at lazabs.horn.bottomup.HornPredAbs.genEdge(HornPredAbs.scala:1421)
        at lazabs.horn.bottomup.HornPredAbs.liftedTree1$1(HornPredAbs.scala:870)
        at lazabs.horn.bottomup.HornPredAbs.<init>(HornPredAbs.scala:869)
        at lazabs.horn.bottomup.InnerHornWrapper$$anonfun$24.apply(HornWrapper.scala:371)
        at lazabs.horn.bottomup.InnerHornWrapper$$anonfun$24.apply(HornWrapper.scala:366)
        at scala.util.DynamicVariable.withValue(DynamicVariable.scala:58)
        at scala.Console$.withOut(Console.scala:65)
        at lazabs.horn.bottomup.InnerHornWrapper.<init>(HornWrapper.scala:366)
        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)

(set-logic HORN)
(declare-fun foo ((_ BitVec 1)) Bool)
(declare-fun bar ((_ BitVec 2)) Bool)
(assert (foo (_ bv1 1)))
(assert
  (forall
    ((x (_ BitVec 1)))
    (=> (foo x) (bar ((_ sign_extend 1) x)))))
(assert
  (forall
    ((x (_ BitVec 2)))
    (=> (bar x) (= x (_ bv3 2)))))
(check-sat)
(get-model)

Warning: ignoring get-model
unsat

0: false -> 1
1: (bar (_ bv1 2)) -> 2
2: (foo (_ bv1 1))

sat
(
  (define-fun bar ((x!0 (_ BitVec 2))) Bool
    (= x!0 #b11))
  (define-fun foo ((x!0 (_ BitVec 1))) Bool
    (= x!0 #b1))
)

Warning: ignoring get-model
Theories: SimpleArray(1)

Initially:                11 clauses
After inlining:           11 clauses
After shortening clauses: 12 clauses

Constant and interval propagation ++++++++++++++++
Unique satisfiable clauses: 12
Starting CEGAR
.
Found counterexample #1, refining ... (2and/0or)  80 -> 79 ... adding predicates:
INV_MAIN_0: !(INV_MAIN_0_13_0 = INV_MAIN_0_4_0) | INV_MAIN_0_14_0 = INV_MAIN_0_5_0

Found counterexample #2, refining ... (2and/0or)  35 -> 34 ... adding predicates:
INV_MAIN_0: !(INV_MAIN_0_13_0 + -1*INV_MAIN_0_11_0 - 4*INV_MAIN_0_10_0 = 0) | !(4*INV_MAIN_0_12_0 + INV_MAIN_0_11_0 - INV_MAIN_0_4_0 = 0) | INV_MAIN_0_14_0 = INV_MAIN_0_5_0

Found counterexample #3, refining ... (2and/0or)  36 -> 35 ... adding predicates:
INV_MAIN_0: !(INV_MAIN_0_11_0 + 4*INV_MAIN_0_10_0 - INV_MAIN_0_4_0 = 0) | INV_MAIN_0_6_0 = INV_MAIN_0_5_0
.
Found counterexample #4, refining ... (2and/0or)  52 -> 51 ... adding predicates:
INV_MAIN_0: !(4*INV_MAIN_0_12_0 + INV_MAIN_0_3_0 - 4*INV_MAIN_0_10_0 - INV_MAIN_0_11_0 = 0), INV_MAIN_0_13_0 + -4*INV_MAIN_0_12_0 - INV_MAIN_0_3_0 = 0

Found counterexample #5, refining ... (3and/0or)  66 -> 65 ... adding predicates:
INV_MAIN_0: INV_MAIN_0_14_0 = INV_MAIN_0_6_0 & INV_MAIN_0_13_0 + -4*INV_MAIN_0_12_0 - INV_MAIN_0_3_0 = 0 & INV_MAIN_0_11_0 = INV_MAIN_0_3_0, !(INV_MAIN_0_13_0 + -4*INV_MAIN_0_10_0 - INV_MAIN_0_3_0 = 0) | !(4*INV_MAIN_0_12_0 + INV_MAIN_0_3_0 - INV_MAIN_0_4_0 = 0) | INV_MAIN_0_6_0 = INV_MAIN_0_5_0
..
Found counterexample #6, refining ... (2and/0or)  60 -> 59 ... adding predicates:
INV_MAIN_0: !(INV_MAIN_0_13_0 = INV_MAIN_0_4_0) | (INV_MAIN_0_11_0 + 4*INV_MAIN_0_10_0 - INV_MAIN_0_4_0 = 0 & INV_MAIN_0_6_0 = INV_MAIN_0_5_0)
..
Found counterexample #7, refining ... (4and/0or)  267 -> 160 ... adding predicates:
INV_MAIN_0_INV_MAIN_0_INV_MAIN_0: !(INV_MAIN_0_INV_MAIN_0_INV_MAIN_0_13_0 = INV_MAIN_0_INV_MAIN_0_INV_MAIN_0_4_0) | INV_MAIN_0_INV_MAIN_0_INV_MAIN_0_14_0 = INV_MAIN_0_INV_MAIN_0_INV_MAIN_0_5_0
.
Found counterexample #8, refining ... (4and/0or) . 420 -> 319 ... adding predicates:
INV_MAIN_0: INV_MAIN_0_11_0 + 4*INV_MAIN_0_7_0 + -1*INV_MAIN_0_3_0 - 4*INV_MAIN_0_0_0 = 0 & INV_MAIN_0_9_0 = INV_MAIN_0_2_0, !(INV_MAIN_0_13_0 = INV_MAIN_0_4_0)
INV_MAIN_0_INV_MAIN_0_INV_MAIN_0: INV_MAIN_0_INV_MAIN_0_INV_MAIN_0_11_0 + 4*INV_MAIN_0_INV_MAIN_0_INV_MAIN_0_7_0 + -1*INV_MAIN_0_INV_MAIN_0_INV_MAIN_0_3_0 - 4*INV_MAIN_0_INV_MAIN_0_INV_MAIN_0_0_0 = 0 & INV_MAIN_0_INV_MAIN_0_INV_MAIN_0_9_0 = INV_MAIN_0_INV_MAIN_0_INV_MAIN_0_2_0, !(INV_MAIN_0_INV_MAIN_0_INV_MAIN_0_43_0 = INV_MAIN_0_INV_MAIN_0_INV_MAIN_0_34_0) | INV_MAIN_0_INV_MAIN_0_INV_MAIN_0_44_0 = INV_MAIN_0_INV_MAIN_0_INV_MAIN_0_35_0
..
Found counterexample #9, refining ... (4and/0or)  205 -> 155java.util.NoSuchElementException: key not found: sc_2_0_0
    at scala.collection.MapLike$class.default(MapLike.scala:228)
    at scala.collection.AbstractMap.default(Map.scala:59)
    at scala.collection.MapLike$class.apply(MapLike.scala:141)
    at scala.collection.AbstractMap.apply(Map.scala:59)
    at ap.util.FastImmutableMap.apply(FastImmutableMap.scala:51)
    at ap.terfor.TermOrder.compareTerms(TermOrder.scala:254)
    at ap.terfor.TermOrder.compare(TermOrder.scala:239)
    at ap.terfor.linearcombination.LinearCombination1.$minus(LinearCombination.scala:1362)
    at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:658)
    at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:546)
    at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:478)
    at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:478)
    at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:478)
    at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:546)
    at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:478)
    at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:515)
    at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:515)
    at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:515)
    at ap.interpolants.Interpolator$.processBranchInferences(Interpolator.scala:515)
    at ap.interpolants.Interpolator$.ap$interpolants$Interpolator$$applyHelp(Interpolator.scala:394)
    at ap.interpolants.Interpolator$.apply(Interpolator.scala:62)
    at lazabs.horn.bottomup.TreeInterpolator$.lazabs$horn$bottomup$TreeInterpolator$$computeInts$1(TreeInterpolator.scala:146)
    at lazabs.horn.bottomup.TreeInterpolator$$anonfun$lazabs$horn$bottomup$TreeInterpolator$$computeInts$1$3.apply(TreeInterpolator.scala:157)
    at lazabs.horn.bottomup.TreeInterpolator$$anonfun$lazabs$horn$bottomup$TreeInterpolator$$computeInts$1$3.apply(TreeInterpolator.scala:156)
    at scala.collection.TraversableLike$WithFilter$$anonfun$map$2.apply(TraversableLike.scala:683)
    at scala.collection.immutable.List.foreach(List.scala:381)
    at scala.collection.TraversableLike$WithFilter.map(TraversableLike.scala:682)
    at lazabs.horn.bottomup.TreeInterpolator$.lazabs$horn$bottomup$TreeInterpolator$$computeInts$1(TreeInterpolator.scala:156)
    at lazabs.horn.bottomup.TreeInterpolator$.treeInterpolate(TreeInterpolator.scala:178)
    at lazabs.horn.bottomup.DisjInterpolator$$anonfun$lazabs$horn$bottomup$DisjInterpolator$$predicateGeneratorHelp$1.apply(DisjInterpolator.scala:607)
    at lazabs.horn.bottomup.DisjInterpolator$$anonfun$lazabs$horn$bottomup$DisjInterpolator$$predicateGeneratorHelp$1.apply(DisjInterpolator.scala:194)
    at ap.SimpleAPI$.withProver(SimpleAPI.scala:142)
    at lazabs.horn.bottomup.DisjInterpolator$.lazabs$horn$bottomup$DisjInterpolator$$predicateGeneratorHelp(DisjInterpolator.scala:194)
    at lazabs.horn.bottomup.DisjInterpolator$$anonfun$predicateGenerator$1.apply$mcV$sp(DisjInterpolator.scala:138)
    at lazabs.horn.bottomup.DisjInterpolator$$anonfun$predicateGenerator$1.apply(DisjInterpolator.scala:138)
    at lazabs.horn.bottomup.DisjInterpolator$$anonfun$predicateGenerator$1.apply(DisjInterpolator.scala:138)
    at scala.util.DynamicVariable.withValue(DynamicVariable.scala:58)
    at ap.util.Timeout$.withChecker(Timeout.scala:44)
    at ap.util.Timeout$$anonfun$withTimeoutMillis$1.apply(Timeout.scala:58)
    at ap.util.Timeout$.catchTimeout(Timeout.scala:88)
    at ap.util.Timeout$.withTimeoutMillis(Timeout.scala:61)
    at lazabs.horn.bottomup.DisjInterpolator$.predicateGenerator(DisjInterpolator.scala:155)
    at lazabs.horn.bottomup.DagInterpolator$.interpolatingPredicateGenCEXAndOr(DagInterpolator.scala:156)
    at lazabs.horn.bottomup.HornWrapper$$anonfun$10$$anonfun$apply$5.apply(HornWrapper.scala:166)
    at lazabs.horn.bottomup.HornWrapper$$anonfun$10$$anonfun$apply$5.apply(HornWrapper.scala:166)
    at lazabs.horn.bottomup.HornPredAbs.liftedTree1$1(HornPredAbs.scala:932)
    at lazabs.horn.bottomup.HornPredAbs.<init>(HornPredAbs.scala:909)
    at lazabs.horn.bottomup.HornWrapper$$anonfun$12.apply(HornWrapper.scala:218)
    at lazabs.horn.bottomup.HornWrapper$$anonfun$12.apply(HornWrapper.scala:218)
    at scala.util.DynamicVariable.withValue(DynamicVariable.scala:58)
    at scala.Console$.withOut(Console.scala:65)
    at lazabs.horn.bottomup.HornWrapper.<init>(HornWrapper.scala:217)
    at lazabs.horn.Solve$.apply(Solve.scala:81)
    at lazabs.Main$$anonfun$doMain$3.apply$mcV$sp(Main.scala:421)
    at lazabs.Main$$anonfun$doMain$3.apply(Main.scala:421)
    at lazabs.Main$$anonfun$doMain$3.apply(Main.scala:421)
    at scala.util.DynamicVariable.withValue(DynamicVariable.scala:58)
    at scala.Console$.withErr(Console.scala:80)
    at lazabs.Main$.doMain(Main.scala:420)
    at lazabs.Main$.main(Main.scala:143)
    at lazabs.Main.main(Main.scala)
    at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
    at sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:62)
    at sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43)
    at java.lang.reflect.Method.invoke(Method.java:498)
    at scala.reflect.internal.util.ScalaClassLoader$$anonfun$run$1.apply(ScalaClassLoader.scala:70)
    at scala.reflect.internal.util.ScalaClassLoader$class.asContext(ScalaClassLoader.scala:31)
    at scala.reflect.internal.util.ScalaClassLoader$URLClassLoader.asContext(ScalaClassLoader.scala:101)
    at scala.reflect.internal.util.ScalaClassLoader$class.run(ScalaClassLoader.scala:70)
    at scala.reflect.internal.util.ScalaClassLoader$URLClassLoader.run(ScalaClassLoader.scala:101)
    at scala.tools.nsc.CommonRunner$class.run(ObjectRunner.scala:22)
    at scala.tools.nsc.ObjectRunner$.run(ObjectRunner.scala:39)
    at scala.tools.nsc.CommonRunner$class.runAndCatch(ObjectRunner.scala:29)
    at scala.tools.nsc.ObjectRunner$.runAndCatch(ObjectRunner.scala:39)
    at scala.tools.nsc.MainGenericRunner.runTarget$1(MainGenericRunner.scala:65)
    at scala.tools.nsc.MainGenericRunner.run$1(MainGenericRunner.scala:87)
    at scala.tools.nsc.MainGenericRunner.process(MainGenericRunner.scala:98)
    at scala.tools.nsc.MainGenericRunner$.main(MainGenericRunner.scala:103)
    at scala.tools.nsc.MainGenericRunner.main(MainGenericRunner.scala)

(set-logic HORN)

(declare-fun |state| ( Bool Bool Bool Bool Int Int Int ) Bool)

(assert (forall ((C Int) (D Int) (E Int)) (state false true false false C D E)))

(assert (forall ((A Bool)
         (B Bool)
         (C Bool)
         (D Bool)
         (E Bool)
         (F Bool)
         (G Int)
         (H Int)
         (I Int)
         (J Int)
         (K Int)
         (L Int)
         (M Bool)
         (N Bool))
  (let ((a!1 (and (state B A N M H J L)
                  (or M N (not A) (not B) (and F D (not C) (= H G)))
                  (or M A B)
                  (or M (not N) A)
                  (or N (not M) (not B))
                  (or M N B (and (not F) E (not D) (= G 1)))
                  (or M N A (and E D (not C) (= H G)))
                  (or N B (<= H 0)))))
    (or (not a!1) (state E D C F G I K)))))
    
(assert (forall ((C Int) (D Int) (E Int)) (not (state false false true true C D E))))

(check-sat)

sat
(define-fun state ((A Bool) (B Bool) (C Bool) (D Bool) (E Int) (F Int) (G Int)) Bool (or (or (or (and (and (and (= A true) (= B true)) (not (= C true))) (>= E 1)) (and (and (= A true) (and (not (= B true)) (not (= D true)))) (>= E 1))) (and (= B true) (and (and (not (= A true)) (not (= C true))) (not (= D true))))) (and (and (= B true) (not (= C true))) (and (>= (- E D) 1) (>= (+ D E) 1)))))

Theories: GroebnerMultiplication, ModuloArithmetic
Exception in thread "main" java.lang.AssertionError: assertion failed
	at scala.Predef$.assert(Predef.scala:156)
	at ap.terfor.arithconj.ReducableModelElement.extendModel(ModelFinder.scala:197)
	at ap.terfor.arithconj.ModelElement$$anonfun$constructModel$1.apply(ModelFinder.scala:55)
	at ap.terfor.arithconj.ModelElement$$anonfun$constructModel$1.apply(ModelFinder.scala:55)
	at scala.collection.immutable.List.foreach(List.scala:392)
	at ap.terfor.arithconj.ModelElement$.constructModel(ModelFinder.scala:55)
	at ap.proof.ModelSearchProver.extractModel$1(ModelSearchProver.scala:730)
	at ap.proof.ModelSearchProver.handleSatGoal(ModelSearchProver.scala:852)
	at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:482)
	at ap.proof.ModelSearchProver.extractModel$1(ModelSearchProver.scala:772)
	at ap.proof.ModelSearchProver.handleSatGoal(ModelSearchProver.scala:852)
	at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:482)
	at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:476)
	at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:589)
	at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:476)
	at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:476)
	at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:476)
	at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:589)
	at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:476)
	at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:476)
	at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:589)
	at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:476)

        at scala.Predef$.assert(Predef.scala:156)                                                                                                                                                  [50/1891]
        at ap.terfor.linearcombination.LinearCombination1.<init>(LinearCombination.scala:1627)
        at ap.terfor.linearcombination.LinearCombination$.apply(LinearCombination.scala:141)
        at ap.parser.InputAbsy2Internal.ap$parser$InputAbsy2Internal$$translateLinComb(InputAbsy2Internal.scala:103)
        at ap.parser.InputAbsy2Internal$$anonfun$ap$parser$InputAbsy2Internal$$translateFor$1.apply(InputAbsy2Internal.scala:115)
        at ap.parser.InputAbsy2Internal$$anonfun$ap$parser$InputAbsy2Internal$$translateFor$1.apply(InputAbsy2Internal.scala:115)
        at scala.collection.Iterator$$anon$11.next(Iterator.scala:410)
        at scala.collection.Iterator$class.foreach(Iterator.scala:891)
        at scala.collection.AbstractIterator.foreach(Iterator.scala:1334)
        at scala.collection.generic.Growable$class.$plus$plus$eq(Growable.scala:59)
        at scala.collection.mutable.ArrayBuilder$ofRef.$plus$plus$eq(ArrayBuilder.scala:99)
        at scala.collection.mutable.ArrayBuilder$ofRef.$plus$plus$eq(ArrayBuilder.scala:56)
        at ap.util.Seqs$.toArray(Seqs.scala:700)                                                                                                                                                   [38/1891]
        at ap.terfor.preds.Atom$.apply(Atom.scala:37)
        at ap.parser.InputAbsy2Internal.ap$parser$InputAbsy2Internal$$translateFor(InputAbsy2Internal.scala:114)
        at ap.parser.InputAbsy2Internal.ap$parser$InputAbsy2Internal$$translateFor(InputAbsy2Internal.scala:112)
        at ap.parser.InputAbsy2Internal.ap$parser$InputAbsy2Internal$$translateFor(InputAbsy2Internal.scala:162)
        at ap.parser.InputAbsy2Internal.ap$parser$InputAbsy2Internal$$translateFor(InputAbsy2Internal.scala:131)
        at ap.parser.InputAbsy2Internal$.apply(InputAbsy2Internal.scala:47)
        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)

'-assert', '-abstract:relEqs'

Theories: ADT(tx_type), ADT(bytes_tuple), SimpleArray(1)
(error "Combination of theories is not supported")

(set-logic HORN)
(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const bv_27-0 (_ BitVec 27))
(declare-const bv_26-0 (_ BitVec 26))
(declare-const bv_14-0 (_ BitVec 14))
(assert (forall ((q0 (_ BitVec 9)) (q1 (_ BitVec 9)) (q2 (_ BitVec 10))) (=> (distinct q2 q2) (= q0 (bvlshr q0 q0)))))
(declare-const bv_12-0 (_ BitVec 12))
(assert (forall ((q14 (_ BitVec 9)) (q15 (_ BitVec 9)) (q16 (_ BitVec 9)) (q17 (_ BitVec 14))) (=> (= (bvnot q15) q16) (distinct q17 (bvurem (bvsub q17 q17) (bvor q17 (bvsub q17 q17)))))))
(assert (forall ((q18 (_ BitVec 9)) (q19 (_ BitVec 9)) (q20 (_ BitVec 26))) (=> (= q20 q20) (bvsge q19 q19))))
(assert (forall ((q22 (_ BitVec 9)) (q23 (_ BitVec 9)) (q24 (_ BitVec 9)) (q25 (_ BitVec 9)) (q26 (_ BitVec 9)) (q27 (_ BitVec 9)) (q28 (_ BitVec 9)) (q29 (_ BitVec 9)) (q30 (_ BitVec 9)) (q31 (_ BitVec 9)) (q32 (_ BitVec 9)) (q33 Bool)) (=> (or q33 q33 q33 q33 q33 q33) (= q23 q23))))
(assert (forall ((q34 (_ BitVec 9)) (q35 (_ BitVec 9)) (q36 (_ BitVec 9)) (q37 (_ BitVec 9)) (q38 (_ BitVec 9)) (q39 (_ BitVec 9)) (q40 (_ BitVec 9)) (q41 (_ BitVec 9)) (q42 (_ BitVec 9)) (q43 (_ BitVec 9)) (q44 (_ BitVec 9)) (q45 (_ BitVec 14))) (=> (bvugt q45 q45) (distinct q35 q37))))
(assert (forall ((q46 (_ BitVec 9)) (q47 (_ BitVec 9)) (q48 (_ BitVec 9)) (q49 (_ BitVec 9)) (q50 (_ BitVec 9)) (q51 (_ BitVec 9)) (q52 Bool)) (=> (= q52 q52 q52 q52 q52 q52 q52) (= q50 (bvand q47 q50)))))
(assert (forall ((q53 (_ BitVec 9)) (q54 (_ BitVec 9)) (q55 (_ BitVec 9)) (q56 (_ BitVec 9)) (q57 (_ BitVec 9)) (q58 (_ BitVec 9)) (q59 (_ BitVec 4))) (=> (= q58 q56) (= q59 q59))))
(assert (forall ((q60 (_ BitVec 9)) (q61 (_ BitVec 9)) (q62 (_ BitVec 27))) (=> (= q62 q62) (= q61 q60))))
(declare-const bv_30-0 (_ BitVec 30))
(assert (forall ((q66 (_ BitVec 9)) (q67 (_ BitVec 9)) (q68 (_ BitVec 9)) (q69 (_ BitVec 9)) (q70 (_ BitVec 9)) (q71 (_ BitVec 9)) (q72 (_ BitVec 9)) (q73 (_ BitVec 9)) (q74 (_ BitVec 9)) (q75 (_ BitVec 9)) (q76 (_ BitVec 9)) (q77 Bool)) (=> (or q77 q77 q77 q77 q77 q77 q77 q77) (distinct q70 q67))))
(assert (forall ((q78 (_ BitVec 9)) (q79 (_ BitVec 26))) (=> (= (bvurem q79 q79) (bvneg q79)) (bvule q78 (bvor q78 q78)))))
(assert (forall ((q80 (_ BitVec 9)) (q81 (_ BitVec 9)) (q82 (_ BitVec 9)) (q83 (_ BitVec 9)) (q84 (_ BitVec 19))) (=> (distinct (bvneg q84) (bvneg q84)) (distinct q80 q82))))
(declare-const bv_14-1 (_ BitVec 14))
(assert (forall ((q86 (_ BitVec 9)) (q87 (_ BitVec 9)) (q88 (_ BitVec 9)) (q89 (_ BitVec 19))) (=> (distinct q88 q86) (= q89 q89))))
(assert (forall ((q90 (_ BitVec 9)) (q91 (_ BitVec 9)) (q92 (_ BitVec 9)) (q93 (_ BitVec 9)) (q94 (_ BitVec 9)) (q95 (_ BitVec 9)) (q96 (_ BitVec 9)) (q97 (_ BitVec 9)) (q98 (_ BitVec 9)) (q99 (_ BitVec 9)) (q100 (_ BitVec 12))) (=> (bvslt q95 q96) (bvslt (bvashr q100 q100) q100))))
(assert (forall ((q101 (_ BitVec 9)) (q102 (_ BitVec 9)) (q103 (_ BitVec 9)) (q104 (_ BitVec 9)) (q105 (_ BitVec 9)) (q106 (_ BitVec 9)) (q107 (_ BitVec 9)) (q108 (_ BitVec 9)) (q109 (_ BitVec 9)) (q110 (_ BitVec 9)) (q111 (_ BitVec 9)) (q112 (_ BitVec 26))) (=> (distinct (bvneg q112) (bvneg q112)) (bvugt q107 q108))))
(check-sat)

'-assert', '-noSlicing', '-abstract:off'

heories: GroebnerMultiplication, ModuloArithmetic
 Exception in thread "main" java.lang.AssertionError: assertion failed
        at scala.Predef$.assert(Predef.scala:156)
        at ap.basetypes.IdealInt.$up(IdealInt.scala:654)
        at ap.theories.bitvectors.ModReducer$Reducer$$anonfun$reduce$1$$anonfun$2.apply(ModReducer.scala:320)
        at ap.theories.bitvectors.ModReducer$Reducer$$anonfun$reduce$1$$anonfun$2.apply(ModReducer.scala:316)
        at ap.util.LRUCache.apply(LRUCache.scala:37)
        at ap.theories.bitvectors.ModReducer$Reducer$$anonfun$reduce$1.apply(ModReducer.scala:315)
        at ap.theories.bitvectors.ModReducer$Reducer$$anonfun$reduce$1.apply(ModReducer.scala:185)
        at ap.terfor.conjunctions.ReducerPlugin$.rewritePreds(ReducerPlugin.scala:89)
        at ap.theories.bitvectors.ModReducer$Reducer.reduce(ModReducer.scala:185)
        at ap.terfor.conjunctions.SeqReducerPlugin.reduce(ReducerPlugin.scala:371)
        at ap.terfor.conjunctions.ReduceWithConjunction.ap$terfor$conjunctions$ReduceWithConjunction$$reduceWithPlugin(ReduceWithConjunction.scala:621)
        at ap.terfor.conjunctions.ReduceWithConjunction$.ap$terfor$conjunctions$ReduceWithConjunction$$reduceConj(ReduceWithConjunction.scala:91)
        at ap.terfor.conjunctions.ReduceWithConjunction$.ap$terfor$conjunctions$ReduceWithConjunction$$reduceConj(ReduceWithConjunction.scala:115)
        at ap.terfor.conjunctions.ReduceWithConjunction$.ap$terfor$conjunctions$ReduceWithConjunction$$reduceConj(ReduceWithConjunction.scala:165)
        at ap.terfor.conjunctions.ReduceWithConjunction$$anonfun$1.apply(ReduceWithConjunction.scala:174)
        at ap.terfor.conjunctions.ReduceWithConjunction$$anonfun$1.apply(ReduceWithConjunction.scala:173)
        at scala.collection.TraversableLike$$anonfun$map$1.apply(TraversableLike.scala:234)
        at scala.collection.TraversableLike$$anonfun$map$1.apply(TraversableLike.scala:234)
        at scala.collection.Iterator$class.foreach(Iterator.scala:891)
        at scala.collection.AbstractIterator.foreach(Iterator.scala:1334)
        at scala.collection.IterableLike$class.foreach(IterableLike.scala:72)
        at ap.terfor.conjunctions.NegatedConjunctions.foreach(NegatedConjunctions.scala:72)
        at scala.collection.TraversableLike$class.map(TraversableLike.scala:234)
        at ap.terfor.conjunctions.NegatedConjunctions.map(NegatedConjunctions.scala:72)
        at ap.terfor.conjunctions.ReduceWithConjunction$.ap$terfor$conjunctions$ReduceWithConjunction$$reduceNegatedConjs(ReduceWithConjunction.scala:173)
        at ap.terfor.conjunctions.ReduceWithConjunction$.ap$terfor$conjunctions$ReduceWithConjunction$$reduceConj(ReduceWithConjunction.scala:99)
        at ap.terfor.conjunctions.ReduceWithConjunction$.ap$terfor$conjunctions$ReduceWithConjunction$$reduceConj(ReduceWithConjunction.scala:165)
        at ap.terfor.conjunctions.ReduceWithConjunction$$anonfun$1.apply(ReduceWithConjunction.scala:174)
        at ap.terfor.conjunctions.ReduceWithConjunction$$anonfun$1.apply(ReduceWithConjunction.scala:173)
        at scala.collection.TraversableLike$$anonfun$map$1.apply(TraversableLike.scala:234)
        at scala.collection.TraversableLike$$anonfun$map$1.apply(TraversableLike.scala:234)
        at scala.collection.Iterator$class.foreach(Iterator.scala:891)
        at scala.collection.AbstractIterator.foreach(Iterator.scala:1334)
        at scala.collection.IterableLike$class.foreach(IterableLike.scala:72)
        at ap.terfor.conjunctions.NegatedConjunctions.foreach(NegatedConjunctions.scala:72)
        at scala.collection.TraversableLike$class.map(TraversableLike.scala:234)

(declare-const c Int)

(assert
(and
(= c (div 5 0))
(not (= c 0))
))

(check-sat)
(get-model)

(set-logic HORN)
(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const bv_15-0 (_ BitVec 15))
(assert (forall ((q1 (_ BitVec 9)) (q2 (_ BitVec 9)) (q3 (_ BitVec 9)) (q4 (_ BitVec 10))) (=> (= q4 q4) (= (bvnor q2 (bvsrem q1 q2)) (bvnor q2 (bvsrem q1 q2))))))
(assert (forall ((q5 (_ BitVec 9)) (q6 (_ BitVec 9)) (q7 (_ BitVec 9)) (q8 (_ BitVec 9)) (q9 (_ BitVec 15))) (=> (= q9 q9) (distinct (bvneg q7) (bvneg q7)))))
(check-sat)
(exit)

 Theories: GroebnerMultiplication, ModuloArithmetic                                                                                                                                                [59/1922]
 Exception in thread "main" java.lang.AssertionError: assertion failed
        at scala.Predef$.assert(Predef.scala:156)
        at ap.terfor.conjunctions.ConjunctEliminator.ap$terfor$conjunctions$ConjunctEliminator$$eliminableDivInEqs(ConjunctEliminator.scala:558)
        at ap.terfor.conjunctions.ConjunctEliminator$$anonfun$eliminate$1.apply(ConjunctEliminator.scala:720)
        at ap.terfor.conjunctions.ConjunctEliminator$$anonfun$eliminate$1.apply(ConjunctEliminator.scala:694)
        at scala.collection.Iterator$class.foreach(Iterator.scala:891)
        at ap.util.FilterIt.foreach(FilterIt.scala:35)
        at ap.terfor.conjunctions.ConjunctEliminator.eliminate(ConjunctEliminator.scala:694)
        at ap.proof.goal.EliminateFactsTask$.apply(EliminateFactsTask.scala:45)
        at ap.proof.goal.Goal.step(Goal.scala:395)
        at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:470)
        at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:476)
        at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:589)
        at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:476)
        at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:589)
        at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:476)
        at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:589)
        at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:476)
        at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:589)
        at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:476)
        at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:589)
        at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:476)
        at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:589)
        at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:476)
...

-assert -noSlicing  -abstract:relIneqs