AssertionError at HornWrapper.scala:73

[rainoftime]

Hi, for this formula

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

Eldaricat f817bc3

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)

[rainoftime]

(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_32-0 (_ BitVec 32))
(assert (forall ((q7 (_ BitVec 10)) (q8 (_ BitVec 10)) (q9 (_ BitVec 10)) (q10 (_ BitVec 10)) (q11 (_ BitVec 10)) (q12 (_ BitVec 10)) (q13 (_ BitVec 10)) (q14 (_ BitVec 10)) (q15 (_ BitVec 32))) (=> (= q9 q7) (bvule (bvlshr q15 q15) q15))))
(assert (forall ((q16 (_ BitVec 10)) (q17 (_ BitVec 10)) (q18 (_ BitVec 10)) (q19 (_ BitVec 10)) (q20 (_ BitVec 10)) (q21 (_ BitVec 10)) (q22 (_ BitVec 32))) (=> (bvugt (bvsdiv q22 q22) (bvsdiv q22 q22)) (= q16 q20))))
(check-sat)

[rainoftime]

(set-logic HORN)
(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const bv_23-0 (_ BitVec 23))
(declare-const bv_34-0 (_ BitVec 34))
(assert (forall ((q0 (_ BitVec 11)) (q1 (_ BitVec 11)) (q2 (_ BitVec 11)) (q3 (_ BitVec 10))) (=> (distinct (bvashr q3 (bvurem q3 q3)) (bvashr q3 (bvurem q3 q3))) (distinct q0 q2))))
(assert (forall ((q4 (_ BitVec 11)) (q5 (_ BitVec 11)) (q6 (_ BitVec 11)) (q7 (_ BitVec 34))) (=> (bvule q5 q5) (bvuge q7 q7))))
(declare-const bv_60-0 (_ BitVec 60))
(assert (forall ((q8 (_ BitVec 11)) (q9 (_ BitVec 11)) (q10 (_ BitVec 11)) (q11 (_ BitVec 11)) (q12 (_ BitVec 34))) (=> (distinct q10 q8) (= q12 q12))))
(check-sat)

[rainoftime]

(set-logic HORN)
(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const bv_43-0 (_ BitVec 43))
(assert (forall ((q3 (_ BitVec 6)) (q4 (_ BitVec 6)) (q5 (_ BitVec 6)) (q6 Bool)) (=> (bvugt (bvsdiv (bvlshr q3 (bvsub q4 q3)) (bvlshr q3 (bvsub q4 q3))) (bvsdiv (bvlshr q3 (bvsub q4 q3)) (bvlshr q3 (bvsub q4 q3)))) (and q6 q6 q6))))
(assert (forall ((q7 (_ BitVec 6)) (q8 (_ BitVec 6)) (q9 (_ BitVec 43))) (=> (distinct (bvudiv q9 q9) q9) (= q7 q7))))
(check-sat)