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
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