dolmen icon indicating copy to clipboard operation
dolmen copied to clipboard

`Cannot find binding for id` in Printers

Open Halbaroth opened this issue 10 months ago • 0 comments

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

Halbaroth avatar Feb 07 '25 10:02 Halbaroth