CodePlexProject Hosting for Open Source Software

1

Closed

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?No files are attached

## comments

leodemoura wrote Apr 9, 2013 at 1:03 AM

https://z3.codeplex.com/SourceControl/changeset/93297fa9e72f750fc8115f0568217f474888563e

The fix is already available in the

`unstable`

(work-in-progress) branch.