Z3Exception: invalid rational value passed as an integer

[daniel-larraz]

I run zustre --timeout 300 with the attached program (z3_exception.zip), and I get the following error:

Process Process-1:
Traceback (most recent call last):
  File "/usr/lib/python2.7/multiprocessing/process.py", line 258, in _bootstrap
    self.run()
  File "/usr/lib/python2.7/multiprocessing/process.py", line 114, in run
    self._target(*self._args, **self._kwargs)
  File "./build/run/bin/zustre", line 76, in main
    zus.encodeAndSolve()
  File "/home/daniel/Projects/Zustre/zustre/build/run/lib/zustrepy/src/zustre.py", line 192, in encodeAndSolve
    res = self.fp.query (q[0])
  File "src/api/python/z3.py", line 6351, in query
  File "src/api/python/z3core.py", line 4613, in Z3_fixedpoint_query
Z3Exception: invalid rational value passed as an integer

A direct call to z3 results in a Segmentation fault:

Term not handled (div0 (to_int aux!12))
Segmentation fault (core dumped)