rainoftime

**src/math/simplex/model_based_opt.cpp:184** ~~~~ (set-logic NRA) (declare-fun r8 () Real) (declare-fun r101 () Real) (declare-fun r104 () Real) (assert (forall ((q1002 Real) (q1003 Bool) (q1004 Real)) (not (

**src/math/simplex/model_based_opt.cpp:183** ~~~~ (set-logic NRA) (declare-fun r12 () Real) (assert (forall ((q385 Bool) (q386 Real)) (not (> (* (* 815.0 0.71478081) r12) 726600630.0 q386)))) (apply qe_rec) ~~~~ ~~~~ z3 xx.smt2 ASSERTION...

At 8ba0fb5b5899b1b2f2b3 An instance without option ~~~~ (declare-fun x0 () (Array Bool Bool)) (assert (forall ((A3 (Array (Array Bool Bool) Bool))) (forall ((A2 (Array Bool Bool))) (let (($x38 (select (store...

Another bit-vector formula ~~~~ (set-logic QF_BV) (declare-fun notes () (_ BitVec 4)) (declare-fun | | () (_ BitVec 4)) (declare-fun || () (_ BitVec 4)) (check-sat) ~~~~

At commit 7625fe26c, NPD.txt is fixed, while NPD2.txt is not

Here is small case ~~~~ (set-logic LRA) (declare-const v0 Bool) (declare-const v1 Bool) (declare-const v2 Bool) (declare-const r1 Real) (declare-const r3 Real) (declare-const r4 Real) (declare-const r6 Real) (declare-const r8...

~~~~ (set-logic QF_LRA) (declare-fun x0 () Real) (declare-fun x1 () Real) (declare-fun x2 () Real) (check-sat) (push 1) (check-sat) (pop 1) (assert (or (= (+ (* 9 x2 ) (*...

A CHC(NIA）formula at 36bcc3483bb ~~~~ (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) (assert (forall ((x Int) (y...

~~~~ (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 (_...

~~~~ (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 (_...