Commit 80334a31 authored by Sylvain Dailler's avatar Sylvain Dailler

Solve stack overflow problem in counterexamples

parent e8a6fe0f
......@@ -26,11 +26,11 @@ module M
goal g7: forall l: mylist. l = Nil
(* use list.List
use list.List
use list.Length
goal g: forall l: list int. length l = 0
*)
(*
(*********************************
......
......@@ -318,8 +318,8 @@ and refine_function ~enc (table: correspondence_table) (term: tterm) =
if Hstr.mem enc v then
term
else
let () = Hstr.add enc v () in
let table = refine_variable_value ~enc table v tree in
Hstr.add enc v ();
let tree = Mstr.find v table in
TCvc4_Variable (Tree tree)
)
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment