This project is read-only.


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


I have applied the purify-arith tactic to the
  (forall ((x Int)) (= (mod x 3) 0)))
and got this
  (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 2:03 AM by leodemoura
Bug has been fixed.


leodemoura wrote Apr 9, 2013 at 2:03 AM

Thanks for reporting this bug. It has been fixed.
The fix is already available in the unstable (work-in-progress) branch.