z3
z3 copied to clipboard
Published
20 hours ago •
Z3Prover
Z3Prover
Incorrect result on NRA formula
Hi, For this formula,
(set-logic NRA)
(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(declare-fun d () Real)
(declare-fun ar () Real)
(declare-fun e () Real)
(declare-fun f () Real)
(declare-fun bc () Real)
(declare-fun g () Real)
(declare-fun h () Real)
(declare-fun i () Real)
(declare-fun j () Real)
(declare-fun k () Real)
(declare-fun bd () Real)
(declare-fun l () Real)
(declare-fun be () Real)
(declare-fun m () Real)
(declare-fun bf () Real)
(declare-fun n () Real)
(declare-fun o () Real)
(declare-fun p () Real)
(declare-fun q () Real)
(declare-fun r () Real)
(declare-fun s () Real)
(declare-fun t () Real)
(declare-fun u () Real)
(declare-fun v () Real)
(declare-fun bh () Real)
(declare-fun w () Real)
(declare-fun x () Real)
(declare-fun y () Real)
(declare-fun z () Real)
(declare-fun aa () Real)
(declare-fun ab () Real)
(declare-fun bg () Real)
(declare-fun ac () Real)
(declare-fun ad () Real)
(declare-fun bb () Real)
(declare-fun ae () Real)
(declare-fun ba () Real)
(declare-fun af () Real)
(declare-fun ag () Real)
(declare-fun ah () Real)
(declare-fun ai () Real)
(declare-fun aj () Real)
(declare-fun ak () Real)
(declare-fun al () Real)
(declare-fun am () Real)
(declare-fun an () Real)
(declare-fun ao () Real)
(declare-fun ap () Real)
(assert
(not
(exists
((v Real))
(=>
(and
(or
(and
(= bg p)
(= (/ 6 l ak) 0)
(= u 0)
(= u 2)
(<
(+
z
(/
(* (- a (- h bh)) (/ 9 a (- h bh)))
(* 2 (- ar (- be bg)))
)
)
ab
)
(= w k)
(< 0 (/ 41 ar (- be bg)))
(>= 0 (- a (- h bh)))
)
(= 0 (- e ag))
)
(<= (- e ag) (- m (- bf bb)))
(<= 0 (- d (/ 66 bc u)))
(< 0 (- m (- bf bb)))
(< 0 ad)
)
(or
(= ab bb)
(=>
(<= 0 o)
(=>
(=>
(<= 0 v o)
(and
(<= ak (* m (/ 40 bf bb)))
(<= 0 (* 3 (- bd z)))
(<=
(+ (* d v) (- f (- bd z)))
0
)
(>= v ad)
)
)
(= (- j ap) 2)
)
)
)
)
)
)
)
(assert
(exists
((aq Real))
(=>
(or
(and
(or
(and
(=>
(<= 0 (- bd z) (- d q))
(and
(<=
0
(+
(* (* 91 ah) z)
(* ah bd)
)
am
)
(< z (- b))
)
)
(< 0 aj)
)
(< aj am)
)
(= bf 2)
(<
(+ (- j) (/ (* al al) (* 2 ah)))
r
)
(< 0 al)
(< al am)
(< 0 ag)
(< 0 am)
)
(< 0 (- b o))
)
(or
(= aa 2)
(< 0 ba)
(<
(*
(/ 0
(+
(* (* 3 ah) (* (/ 99 d q) (/ 101 d q)))
(/ (* 2 (- d q)) aj)
(* 2 ba)
)
)
(/
(*
(+
(* ah (- q d))
aj
)
(+
(* (/ (- 1) ah) (- d q))
aj
)
)
(* 2 ah)
)
)
0
)
)
)
)
)
(assert (= a (+ n ak)))
(assert (= b (+ o ao)))
(assert (= c (+ p aj)))
(assert (= d (* q af)))
(assert (= e (/ s ag)))
(assert (= f (+ t an)))
(assert (= bc (+ u af)))
(assert (= g (+ v af)))
(assert (= h (+ bh ak)))
(assert (= i (+ w af)))
(assert (= j (+ x ap)))
(assert (= k (* y am)))
(assert (= bd (+ z an)))
(assert (= l (+ aa ak ab ao)))
(assert (= be (+ bg ae)))
(assert (= m (+ ac ai)))
(assert (= bf (+ bb ai)))
(check-sat)
(get-model)
Z3 will incorrectly report sat, and give a model:
(define-fun ag () Real
(- 1.0))
(define-fun s () Real
1.0)
(define-fun al () Real
(- (/ 1.0 2.0)))
(define-fun ah () Real
1.0)
(define-fun aj () Real
(/ 1.0 2.0))
(define-fun q () Real
(- 2.0))
(define-fun d () Real
(- 1.0))
(define-fun ba () Real
(/ 1.0 8.0))
(define-fun ar () Real
(- 1.0))
(define-fun bh () Real
(/ 1.0 8.0))
(define-fun h () Real
(/ 1.0 8.0))
(define-fun a () Real
1.0)
(define-fun bg () Real
(- 1.0))
(define-fun be () Real
(- (/ 1.0 4.0)))
(define-fun l () Real
0.0)
(define-fun bb () Real
(/ 1.0 8.0))
(define-fun bf () Real
(- (/ 1.0 8.0)))
(define-fun u () Real
(- (/ 1.0 4.0)))
(define-fun bc () Real
(/ 1.0 4.0))
(define-fun ai () Real
(- (/ 1.0 4.0)))
(define-fun ac () Real
(/ 1.0 8.0))
(define-fun m () Real
(- (/ 1.0 8.0)))
(define-fun ae () Real
(/ 3.0 4.0))
(define-fun ao () Real
(- 1.0))
(define-fun ab () Real
(- 1.0))
(define-fun ak () Real
0.0)
(define-fun aa () Real
2.0)
(define-fun an () Real
1.0)
(define-fun z () Real
(/ 1.0 2.0))
(define-fun bd () Real
(/ 3.0 2.0))
(define-fun y () Real
(- (/ 1.0 4.0)))
(define-fun am () Real
(- 1.0))
(define-fun k () Real
(/ 1.0 4.0))
(define-fun ap () Real
0.0)
(define-fun x () Real
1.0)
(define-fun j () Real
1.0)
(define-fun af () Real
(/ 1.0 2.0))
(define-fun w () Real
(/ 1.0 4.0))
(define-fun i () Real
(/ 3.0 4.0))
(define-fun v () Real
(/ 1.0 2.0))
(define-fun g () Real
1.0)
(define-fun t () Real
(- (/ 9.0 8.0)))
(define-fun f () Real
(- (/ 1.0 8.0)))
(define-fun e () Real
(- 1.0))
(define-fun p () Real
(/ 1.0 8.0))
(define-fun c () Real
(/ 5.0 8.0))
(define-fun o () Real
1.0)
(define-fun b () Real
0.0)
(define-fun n () Real
1.0)
(define-fun r () Real
(- (/ 1.0 4.0)))
(define-fun ad () Real
1.0)
If I feed this model to the formula, z3 will report unsat.
OS: Ubuntu 18.04 Revision: a635049
note: the root cause seems to be within the nlsat_solver as the lemma validation fails mid-stream.
(set-logic QF_NRA)
(declare-fun skoS2 () Real)
(declare-fun skoSP () Real)
(declare-fun skoSM () Real)
(declare-fun skoX () Real)
(declare-fun AJOntN () Real)
(declare-fun i0vABO () Real)
(declare-fun LpLYU4 () Real)
(declare-fun WeThA7 () Real)
(assert (<= (- 40.27480555072409) WeThA7))
(assert (<= WeThA7 46.0420390104799))
(assert (<= (- 2.5024609913331304) AJOntN))
(assert (<= AJOntN 34.46083052901105))
(assert (and (not (= skoX (+ 1 (* skoSM (* skoSM (- 1))))))
(and (= (+ (- 1) (* skoSP skoSP)) skoX) (and (= (* skoS2 skoS2) 2)
(and (not (<= skoX 0)) (and (not (<= (- (- WeThA7) LpLYU4) 0))
(and (not (<= skoSM 0)) (and (and (>= skoS2 skoSP)
(= (- (- AJOntN) i0vABO) (- LpLYU4 skoS2)))
(not (<= 1 skoX)))
)
))))))
(check-sat)