You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Hi
I installed kittel-koat (My environment is Mac OS X 10.12.3). I am able to run kittel. E.g. 'kittel.native -smt-solver yices2 cexamples/ex01.koat ' works fine.
But running koat on the same example gives an error.
Hi
I installed kittel-koat (My environment is Mac OS X 10.12.3). I am able to run kittel. E.g. 'kittel.native -smt-solver yices2 cexamples/ex01.koat ' works fine.
But running koat on the same example gives an error.
koat.native -smt-solver yices2 cexamples/ex01.koat
/var/folders/cg/4npp21_d71j2b_fbxyj5l4740000gp/T/FORMULA_1_dd5efa.smt: invalid token . (line 5, column 18)
Fatal error: exception End_of_file
Adding -log 5 to the query gives:
koat.native -smt-solver yices2 cexamples/ex01.koat
/var/folders/cg/4npp21_d71j2b_fbxyj5l4740000gp/T/FORMULA_1_dd5efa.smt: invalid token . (line 5, column 18)
Fatal error: exception End_of_file
cbit-pc708:kittel-koat jpg$ koat.native -smt-solver yices2 -log 5 cexamples/ex01.koat
0.04 LOG: Trying Unsat Transition Removal processor...
0.07 LOG: Trying leaf removal processor ...
0.07 LOG: Trying Unreachable Removal processor...
0.07 LOG: Trying Knowledge Propagation processor...
0.07 LOG: Checking if parts of the problems can be separated out.
0.07 LOG: Considering location subset []
0.07 LOG: Considering location subset [g]
0.07 LOG: Considering location subset []
0.07 LOG: Considering location subset [f]
0.07 LOG: Trying linear PRF (Farkas-based) processor for degree 0 (without size bounds, without minimal element)...
0.08 LOG: Found the following PRF:
Pol(start) = 1
Pol(f) = 1
Pol(g) = 0
0.08 LOG: PRF synthesis successful, proven complexity 1.
0.08 LOG: Trying Unreachable Removal processor...
0.08 LOG: Trying Knowledge Propagation processor...
0.08 LOG: Trying linear PRF (Farkas-based) processor for degree 0 (without size bounds, without minimal element)...
0.08 LOG: Computing RVG.
/var/folders/cg/4npp21_d71j2b_fbxyj5l4740000gp/T/FORMULA_1_1e5a03.smt: invalid token . (line 5, column 18)
Fatal error: exception End_of_file
The text was updated successfully, but these errors were encountered: