jfs-smt2cxx can't handle all formulas that jfs can

[moyix]

There seems to be a slight mismatch in the set of formulas accepted by jfs-smt2cxx versus jfs. An example is 20170501-Heizmann-UltimateAutomizer/cos_polynomial_true-unreach-call.c_9.smt2 (attached), which is quickly solved using jfs but dies with unsupported kind under jfs-smt2cxx:

user@ccbb42e224b5:~$ jfs/build/bin/jfs /out/20170501-Heizmann-UltimateAutomizer/cos_polynomial_true-unreach-call.c_9.smt2 
sat
user@ccbb42e224b5:~$ jfs/build/bin/jfs-smt2cxx /out/20170501-Heizmann-UltimateAutomizer/cos_polynomial_true-unreach-call.c_9.smt2 
unsupported kind
UNREACHABLE executed at /home/user/jfs/src/lib/Core/Z3ASTVisitor.cpp:237!
Aborted (core dumped)

I'll try to look into this more when I have some time but thought I'd file the issue in case it was instantly obvious what was going wrong.

cos_polynomial_true-unreach-call.c_9.txt

[delcypher]

The jfs-smt2cxx tool doesn't run any simplifications passes over the constraints. jfs does run simplifications passes so its likely the simplification passes remove the expression that is causing the crash. To work around this you can use the jfs-opt tool to run the simplification passes that jfs normally runs and then pass the output to jfs-smt2cxx.

It would be useful to know which expression is causing the crash though because ideally we don't want jfs-smt2cxx to crash like this.

[moyix]

Aha, that does explain it. After diffing the output of jfs-opt and jfs-opt -standard-passes, the culprit seems to be this line:

((_ to_fp 11 53) roundNearestTiesToEven (/ 1.0 2.0))

which gets simplified to

(fp #b0 #b01111111110 #x0000000000000)

[delcypher]

It's most likely the (/ 1.0 2.0) that's causing the problem. The type (sort in SMT-LIB parlance) there looks like a real number (not supported by JFS) rather than a floating-point number.