diff --git a/tests/print/smtlib/poly/poly.expected b/tests/print/smtlib/poly/poly.expected index eff09c5de..ddcc691ed 100644 --- a/tests/print/smtlib/poly/poly.expected +++ b/tests/print/smtlib/poly/poly.expected @@ -1 +1,3 @@ -run 'make promote' to update this file \ No newline at end of file +(set-logic QF_UF) +(declare-fun match_bool (par (|'a|) (Bool |'a| |'a|) |'a|)) +(exit) diff --git a/tests/print/smtlib/v2.6/poly.expected b/tests/print/smtlib/v2.6/poly.expected index eff09c5de..84b2650ac 100644 --- a/tests/print/smtlib/v2.6/poly.expected +++ b/tests/print/smtlib/v2.6/poly.expected @@ -1 +1,13 @@ -run 'make promote' to update this file \ No newline at end of file +(set-logic QF_UF) +Error Uncaught exception: + Dolmen_smtlib2_v6_script__Print.Cannot_print("polymorphic function declaration") +Raised at Dolmen_smtlib2_v6_script__Print._cannot_print.(fun) in file "src/languages/smtlib2/v2.6/script/print.ml", line 16, characters 31-55 +Called from Stdlib__Format.output_acc in file "format.ml", line 1355, characters 4-20 +Called from Stdlib__Format.kfprintf.(fun) in file "format.ml", line 1416, characters 16-34 +Called from Dolmen_loop__Export.Smtlib2.pp_stmt in file "src/loop/export.ml", line 263, characters 4-40 +Called from Stdlib__List.fold_left in file "list.ml", line 123, characters 24-34 +Called from Dolmen_loop__Export.Make.export.(fun) in file "src/loop/export.ml", line 645, 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", line 644, characters 8-208 +Called from Dolmen_loop__Pipeline.Make.eval_op in file "src/loop/pipeline.ml", line 87, characters 8-17 +