ucsd-progsys/liquid-fixpoint — pull request #36 by nikivazou (2014-06-17 16:26:56+00:00)
Title: Reals

Adds support for real numbers. See [external/fixpoint/tests/div.fq](https://github.com/ucsd-progsys/liquid-fixpoint/blob/831f0d1f2b1b327d4c6bf34363b1a9d2b0b29de9/external/fixpoint/tests/div.fq) for an example.

Z3 automatically uses nlsat to reason about real numbers which is complete when the query contains only bools and reals.

Note about completeness:
* when integers and reals are mixed z3 is unpredictable
* 0 is an int while 0.0 is a real

So the following returns unknown
~~~
(declare-const x Real)
(assert (not (= x 0)))
(assert (not (= 1 (* x (/ 1 x)))))
(check-sat)
~~~

while the following is UNSAT
~~~
(declare-const x Real)
(assert (not (= x 0.0)))
(assert (not (= 1.0 (* x (/ 1.0 x)))))
(check-sat)
~~~