search

Z3Prover / z3

The Z3 Theorem Prover
Other
10.42k stars 1.47k forks source link

Capability regression for smt.arith.solver 2, 6 #4220

Closed rainoftime closed 4 years ago

rainoftime commented 4 years ago

Hi, for the formula below, z3 (commit f2449df06e) smt.arith.sovler=2 can solve quickly

sat
real    0m0.616s
user    0m0.260s
sys     0m0.028s

, but smt.arith.sovler=6 just returns "unknown"

(smt :num-exprs 89 :num-asts 385 :time 0.18 :before-memory 2.52 :after-memory 2.54)
(tactic-exception "smt tactic failed to show goal to be sat/unsat (incomplete (theory arithmetic))")
unknown
real    0m0.847s
user    0m0.296s
sys     0m0.036s
(set-logic QF_UFNRA)
(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const v3 Bool)
(declare-const v4 Bool)
(declare-const v5 Bool)
(declare-const v6 Bool)
(declare-const r0 Real)
(declare-sort S0 0)
(declare-sort S1 0)
(declare-const v7 Bool)
(declare-const v8 Bool)
(declare-const r2 Real)
(declare-const v9 Bool)
(declare-const v10 Bool)
(declare-const S0-0 S0)
(declare-const r3 Real)
(declare-const S0-1 S0)
(declare-sort S2 0)
(declare-sort S3 0)
(declare-sort S4 0)
(declare-const r4 Real)
(declare-const r5 Real)
(declare-const S1-0 S1)
(declare-const v11 Bool)
(declare-const v12 Bool)
(declare-const v13 Bool)
(declare-const v14 Bool)
(declare-const v15 Bool)
(declare-const v16 Bool)
(declare-const r6 Real)
(declare-const v17 Bool)
(declare-const r7 Real)
(declare-const v18 Bool)
(declare-const r8 Real)
(declare-const S3-0 S3)
(assert (or (or (= S0-1 S0-0 S0-1 S0-1) v18 (= (< r2 0.0) (= v11 v8 v12 (xor v3 v7 (<= r0 r0 676748736.0) v5 v1 v0 true true v4 true) (>= 676748736.0 r2 (/ r3 r4) 0.0) (=> v4 (xor v3 v7 (<= r0 r0 676748736.0) v5 v1 v0 true true v4 true))))) false))
(assert (or (or (> 0.0 0.0 r2) true (> 0.0 0.0 r2)) false))
(assert (or (or (< (/ (- r3) (* 676748736.0 (/ r0 676748736.0) (/ r0 676748736.0) r3)) (* 676748736.0 (/ r0 676748736.0) (/ r0 676748736.0) r3) 5047773.0) (= r2 (/ r0 676748736.0) 676748736.0 (* 676748736.0 (/ r0 676748736.0) (/ r0 676748736.0) r3) (* 676748736.0 (/ r0 676748736.0) (/ r0 676748736.0) r3)) v12) false))
(assert (or (or (xor v3 v7 (<= r0 r0 676748736.0) v5 v1 v0 true true v4 true) v0 v2) false))
(check-sat)
levnach commented 4 years ago

Solved with the monomial bound propagation ./z3 4220.smt2 -st smt.arith.solver=6 smt.arith.nl.bp=true