Getting different sat-answers for local and rise4fun versions of Z3

Jul 25, 2014 at 8:53 AM
Edited Jul 25, 2014 at 12:01 PM
I'm getting various answers for the same formula on my local machine and on rise4fun. I tested on this SMT-LIB 2 file:
(declare-fun x () Int)
(declare-fun mul () Real)
(declare-fun mul1 () Real)
(declare-fun div1 () Real)
(declare-fun div6 () Real)
(declare-fun add () Real)
(declare-fun cmp () Bool)
(declare-fun call () Real)
(assert (and (= mul (* (- 1.0) x))
     (= mul1 (* mul x))
     (= div6 (* (/ 1.0 2.0) mul1))
     (= add (+ 1.0 div6))
     (= div1 (/ div6 add))
     (= cmp (not (<= call (/ 1.0 1000.0))))
     cmp))
(check-sat)
(get-model)
(exit)
On my local machine (Linux x64) Z3 is built from the latest revision of unstable branch. On request (check-sat) Z3 answers "unknown".
Rise4Fun version of Z3 successfully answers "sat" and generates model for this formula.

What could be the reason for this differences?
What version of Z3 is installed on rise4fun?
Coordinator
Jul 25, 2014 at 12:47 PM
Thanks for reporting this issue! The version of Z3 running on rise4fun is not the latest unstable, but an older unstable version (but newer than the master branch). Updating the binary on rise4fun is not automated, so it's hard to keep them in sync.
Aug 8, 2014 at 2:57 PM
I can't reproduce this issue again. Now both on my local Z3 and on rise4fun Z3 I'm getting "unknown" answer for the example above.
Did you updated Z3 version on rise4fun?
Can you tell exactly what version of Z3 was there on rise4fun? 32-bit or 64-bit?
Did you check my issue when i reported it? I'm not sure by now that it was valid(((
Coordinator
Aug 8, 2014 at 3:12 PM
Yes, the binary on rise4fun was updated some time in the last three days. There's no way to tell what version used to be there, but it was definitely an older version in which some of the later bugfixes were not included yet (although the binary on rise4fun should always have been a 32-bit version, I think). Thanks for checking whether it still reproduces!