search

Z3Prover / z3

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

(debug) refutation unsoundness #4986

Closed muchang closed 3 years ago

muchang commented 3 years ago

Hi, here is a refutation soundness bug that is only on the debug build:

[619] % z3release small.smt2
sat
[620] % cvc4 -q small.smt2
sat
[621] % z3debug small.smt2
unsat
[622] % 
[622] % cat small.smt2
(declare-fun a () Int)
(declare-fun b () Int)
(declare-fun c () Int)
(declare-fun d () Int)
(declare-fun e () Int)
(declare-fun f () Int)
(declare-fun g () Int)
(declare-fun h () Int)
(declare-fun i () Int)
(declare-fun j () Int)
(declare-fun k () Int)
(declare-fun l () Int)
(declare-fun m () Int)
(declare-fun n () Int)
(declare-fun o () Int)
(declare-fun p () Int)
(assert
 (or
 (and (>= m 0)
  (> (* i d) 0)
  (= (mod 1 c) 0)
  (>= c 0)
  (>= d 0)
  (= (+ (- m) a (* e d)) (+ c (* f d)) 0))))
(assert (<= (+ (* a o) j) 0 (+ i (* e o) (* f j)) 0))
(assert
 (or
 (and (>= g 0 p l (* h k) 0)
  (= (+ g (* a k) (+ e l))
  (+ (- 1) k (* f l))
  (+ g (* b k) 2 (* n k))
  0))))
(check-sat)
[623] %

Commit: 20870c4

NikolajBjorner commented 3 years ago

similar to other nlsat

muchang commented 3 years ago

Thanks, moved to: https://github.com/Z3Prover/z3/issues/4804#issuecomment-771537271