Soundness bug with rewriter.arith_ineq_lhs true,rewriter.hoist_cmul true, model_evaluator.array_equalities false

[wintered]

[644] % z3 small.smt2 
sat
[645] % 
[645] % cat small.smt2 
(set-option :rewriter.arith_ineq_lhs true)
(set-option :rewriter.hoist_cmul true)
(set-option :model_evaluator.array_equalities false)
(assert (forall ((x Real)) (forall ((y Int)) (xor (< y x) (<= y (* 236 x (- 114)))))))
(check-sat)
[646] %

OS: Ubuntu 18.04
Commit: cb13641

[NikolajBjorner]

must have been a duplicate of the recent regression

[zhendongsu]

Nikolaj, I can still reproduce the bug on the latest commit (both debug and release builds):

[852] % z3 bug3836.smt2 
sat
[853] % z3release bug3836.smt2 
sat
[854] % cat bug3836.smt2 
(set-option :rewriter.arith_ineq_lhs true)
(set-option :rewriter.hoist_cmul true)
(set-option :model_evaluator.array_equalities false)
(assert (forall ((x Real)) (forall ((y Int)) (xor (< y x) (<= y (* 236 x (- 114)))))))
(check-sat)
[855] % 

@NikolajBjorner

[zhendongsu]

I have the following very similar instance that is failing, which was why I double-checked this one:

[859] % z3 small.smt2 
sat
[860] % z3release small.smt2 
sat
[861] % cat small.smt2 
(set-option :rewriter.arith_ineq_lhs true)
(set-option :rewriter.hoist_cmul true)
(set-option :model_evaluator.array_equalities false)
(declare-fun x () Real)
(assert (< x 0))
(assert (forall ((y Real)) (xor (> y 1) (<= y x))))
(check-sat)
[862] %