Soundness bug default mode unsat (incorrect), ewriter.eq2ineq=true sat (correct)

[wintered]

[644] % z3 rewriter.eq2ineq=true small.smt2 
sat
[645] % z3 small.smt2
unsat
[646] % cat small.smt2
(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(declare-fun d () Real)
(assert
 (forall ((e Real))
 (not
  (=>
  (= (<= (- 2) e b) (>= c (* e e)))
  (= c (* (- (+ a 1) d) (- (+ a 1) d)))
  (= d 0)))))
(check-sat)
[647] %

OS: Ubuntu 18.04
Commit: 3a63c37

[wintered]

[658] % z3 rewriter.eq2ineq=true t.smt2 
sat
(model 
 (define-fun c () Real
  4.0)
 (define-fun a () Real
  (- 2.0))
 (define-fun d () Real
  1.0)
 (define-fun b () Real
  2.0)
)
[659] % z3 s.smt2 
sat
(model 
)
[660] % cat t.smt2 
(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(declare-fun d () Real)
(assert
 (forall ((e Real))
 (not
  (=>
  (= (<= (- 2) e b) (>= c (* e e)))
  (= c (* (- (+ a 1) d) (- (+ a 1) d)))
  (= d 0)))))
(check-sat)
(get-model)
[661] % cat s.smt2 
(define-fun c () Real 4.0)
(define-fun a () Real (- 2.0))
(define-fun d () Real 1.0)
(define-fun b () Real 2.0)
(assert
 (forall ((e Real))
 (not
  (=>
  (= (<= (- 2) e b) (>= c (* e e)))
  (= c (* (- (+ a 1) d) (- (+ a 1) d)))
  (= d 0)))))
(check-sat)
(get-model)
[662] %

[NikolajBjorner]

#2650

[zhendongsu]

Nikolaj, I assume that you want us to add it to #2650, not that you believe that it is a duplicate of it, correct?

[NikolajBjorner]

probable duplicate root cause. At any rate #2650 related bugs better be collected one place to avoid noise.

[zhendongsu]

Okay, Nikolaj, from now on, we'll remember to add any soundness bugs involving non-linear arithmetic to #2650 until it is fixed. We did use nlsat.check_lemmas=true to double-check as you suggested earlier (for this one and #4096), but no assertion violations, segfaults, or validation failures occurred.

[NikolajBjorner]

yes, I checked as well before adding comment. Nevertheless, it is more productive to focus on #2650 for things related to nlsat unsoundness