Gbury / dolmen

Dolmen provides a library and a binary to parse, typecheck, and evaluate languages used in automated deduction
BSD 2-Clause "Simplified" License
79 stars 16 forks source link

Uncaught exception on buggy file #191

Closed Stevendeo closed 11 months ago

Stevendeo commented 11 months ago

The following (wrong) file raises an internal error:

(declare-fun float (Int, Int) Real)

Error: ->

Error Uncaught exception:
      Failure("lexing: empty token")
Raised by primitive operation at file "lexing.ml", line 75, characters 15-41
Called from file "src/languages/smtlib2/v2.6/script/lexer.ml", line 485, characters 8-69
Called from file "src/standard/transformer.ml", line 94, characters 18-44
Called from file "src/languages/smtlib2/v2.6/script/parser.ml", line 3529, characters 19-47
Called from file "src/standard/transformer.ml", line 100, characters 18-41

I know there should be no ',' between the types in the function declaration, but I thought you might want to address the issue anyway.