1

Closed

Elimination of mod terms in integer formulae introduces a variable of sort "real"

description

I have applied the purify-arith tactic to the
(goal
  (forall ((x Int)) (= (mod x 3) 0)))
and got this
(goal
  (forall ((x Int))
    (exists ((x!0 Real)) (and (= x!0 0) (<= 0 x) (not (<= 3 x)) (= x 0)))))
It seems strange that the introduced quantifier bounds a real variable. It's not the expected behavior, is it?
Closed Apr 9, 2013 at 1:03 AM by leodemoura
Bug has been fixed.

comments

leodemoura wrote Apr 9, 2013 at 1:03 AM

Thanks for reporting this bug. It has been fixed.
https://z3.codeplex.com/SourceControl/changeset/93297fa9e72f750fc8115f0568217f474888563e
The fix is already available in the unstable (work-in-progress) branch.