Hi,
for this formula z3 gives a wrong model
(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(declare-fun d () Real)
(declare-fun e () Real)
(declare-fun f () Real)
(declare-fun g () Real)
(declare-fun h () Real)
(declare-fun i () Real)
(declare-fun j () Real)
(declare-fun k () Real)
(assert
(not
(exists
((l Real))
(=>
(and
(=
(<= 0 l)
(>= (+ (* e l) (/ c j)) 0)
)
(>= (/ b i) 0)
)
(<=
(- d g)
(*
(/ 1 2)
(+
(* e (* (/ b i) (/ b i)))
(* (* 2 (/ b i)) k)
(* 2 (- d g))
)
)
)
)
)
)
)
(assert (= h (/ a e) (* f f)))
(assert (= k (/ c j) (/ c k)))
(check-sat)
(get-model)
Model:
(define-fun k () Real
(- (/ 1.0 4.0)))
(define-fun c () Real
(/ 1.0 16.0))
(define-fun j () Real
(- (/ 1.0 4.0)))
(define-fun a () Real
(- 1.0))
(define-fun e () Real
0.0)
(define-fun b () Real
(- 1.0))
(define-fun i () Real
(- 1.0))
(define-fun f () Real
(- 1.0))
(define-fun h () Real
1.0)
(define-fun d () Real
0.0)
(define-fun g () Real
0.0)
The model is wrong since the first and evaluates to false as -1/4 >= 0 does not hold for
(>= (+ (* e l) (/ c j)) 0). In turn, the outermost (=> evaluates to true which is negated by a not, i.e. the first assertion simplifies to false. Feeding the model to the formula results in an assertion violation
ASSERTION VIOLATION
File: ../src/qe/qsat.cpp
Line: 631
validate_defs("check_sat")
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
Revision: 000e485 (assertions enabled)
OS: Ubuntu 18.04
Hi,
for this formula z3 gives a wrong model
Model:
The model is wrong since the first
andevaluates tofalseas-1/4 >= 0does not hold for(>= (+ (* e l) (/ c j)) 0). In turn, the outermost(=>evaluates to true which is negated by anot, i.e. the first assertion simplifies to false. Feeding the model to the formula results in an assertion violationRevision: 000e485 (assertions enabled)
OS: Ubuntu 18.04