Closed dddejan closed 8 years ago
Running the solver on the problem below I get a parse error.
(set-logic QF_LIA) (declare-fun x () Int) (declare-fun y () Int) (assert (and (<= 0 x) (<= x 10)) (assert (= y (# u Int (= y x))) (check-sat) (get-model)
The error is
dejan@pup:~/workspace/counting-smt$ ./solver.native --verbose < ./examples/test04.smt2 -> (set-logic QF_LIA) -> (declare-fun x () Int) -> (declare-fun y () Int) Fatal error: exception Lisp_lexer.SyntaxError("Unexpected char: <")
If possible it would be good to output some more info on the error.
Running the solver on the problem below I get a parse error.
The error is
If possible it would be good to output some more info on the error.