Skip to content

Cannot find binding for id in Printers #226

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

Open
Halbaroth opened this issue Feb 7, 2025 · 0 comments
Open

Cannot find binding for id in Printers #226

Halbaroth opened this issue Feb 7, 2025 · 0 comments

Comments

@Halbaroth
Copy link
Contributor

Printers of #211 work on many Alt-Ergo files after disabling logic detection, as in #225. However, some files still cause Dolmen to raise uncaught exceptions. For instance, on the following file:

logic f : 'a -> 'a
axiom a : exists x:'a. x = f(x)
goal g : false

I got

Error Uncaught exception:
      Failure("cannot find binding for id")
Raised at Stdlib.failwith in file "stdlib.ml", line 29, characters 17-33
Called from Dolmen_smtlib2_poly__Print.Make.ty_var in file "src/languages/smtlib2/poly/print.ml", line 322, characters 15-36
Called from Stdlib__List.iter in file "list.ml", line 112, characters 12-15
Called from Stdlib__Format.output_acc in file "format.ml", line 1395, characters 32-48
Called from Stdlib__Format.output_acc in file "format.ml", line 1383, characters 4-20
Called from Stdlib__Format.output_acc in file "format.ml", line 1396, characters 32-48
Called from Stdlib__Format.output_acc in file "format.ml", line 1395, characters 32-48
Called from Stdlib__Format.output_acc in file "format.ml", line 1383, characters 4-20
Called from Stdlib__Format.kfprintf.(fun) in file "format.ml", line 1444, characters 16-34
Called from Stdlib__Format.output_acc in file "format.ml", line 1395, characters 32-48
Called from Stdlib__Format.output_acc in file "format.ml", line 1383, characters 4-20
Called from Stdlib__Format.kfprintf.(fun) in file "format.ml", line 1444, characters 16-34
Called from Stdlib__Format.output_acc in file "format.ml", line 1383, characters 4-20
Called from Stdlib__Format.kfprintf.(fun) in file "format.ml", line 1444, characters 16-34
Called from Dolmen_loop__Export.Smtlib2.pp_stmt in file "src/loop/export.ml", line 287, characters 6-42
Called from Dolmen_loop__Export.Make.export.(fun) in file "src/loop/export.ml", line 700, characters 26-45
Called from Stdlib__List.fold_left in file "list.ml", line 123, characters 24-34
Called from Dolmen_loop__Export.Make.export in file "src/loop/export.ml", lines 699-703, characters 8-23
Called from Dolmen_loop__Pipeline.Make.eval_op in file "src/loop/pipeline.ml", line 87, characters 8-17
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