rainoftime
rainoftime
Also related to Boolean variables
If there are Boolean variables, and the real invariable occurs in the assertion, then there will be this error
Thank you!
at exists_forall/ef_values.c:730: ~~~~ (set-logic UF) (declare-fun v () Bool) (declare-sort S 0) (assert (or (forall ((q Bool)) (exists ((q2 S)) (forall ((q S)) (distinct v (not (= q2 q)))))))) (assert...
38250fc304ab66bf39613e669 ~~~~ (declare-const x Bool) (declare-fun n () Real) (declare-fun d () Real) (declare-fun i () Real) (declare-fun h () Real) (declare-fun f () Real) (declare-fun g () Real) (assert...
Soundness issue at commit ed3f8a52e6f010d14f9bfca39 ~~~~ (declare-fun n () Real) (declare-fun d () Real) (declare-fun i () Real) (declare-fun h () Real) (declare-fun c () Real) (declare-fun f () Real)...
A QF_LRA formula at commit f370d8d9b4f ~~~~ (set-logic QF_LRA) (declare-const r0 Real) (declare-const r1 Real) (assert (< r0 0.0 r1 0.955441)) (maximize r1) (check-sat) (get-objectives) ~~~~ ~~~~ ./z3 smt.arith.solver=6 xx.smt2...
For smtlib2 instance by @amchiclet , both smt.arith.solver=6 and smt.arith.solver=2 can return 189 (at commit f370d8d) Perhaps the version in rise4fun is different from 4.8.8.0.
ba5c9c3883, the results of arith.solver=2 and =6 seem different ~~~~ (set-logic QF_LIA) (declare-const i2 Int) (declare-const i4 Int) (assert (
@delcypher @NikolajBjorner I believe further efforts are deserved to make z3's build system more flexible and adjustable. Suppose a user only needs the bit-blasting based bit-vector solver(`qfbv_tactic`), it seems we...