Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Koat crashing #13

Open
jpgallagher opened this issue Mar 10, 2017 · 0 comments
Open

Koat crashing #13

jpgallagher opened this issue Mar 10, 2017 · 0 comments

Comments

@jpgallagher
Copy link

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

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant