From 47a0b075f06e177e8bb8bcb918da54e3a99ff776 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Thu, 1 Sep 2022 22:33:59 -0400 Subject: [PATCH] fix(model builder): allow multiple `add` --- src/smt/model_builder.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/smt/model_builder.ml b/src/smt/model_builder.ml index 7c6af253..32790e34 100644 --- a/src/smt/model_builder.ml +++ b/src/smt/model_builder.ml @@ -37,10 +37,10 @@ let require_eval (self : t) t : unit = let mem self t : bool = T.Tbl.mem self.m t let add (self : t) ?(subs = []) t v : unit = - assert (not @@ T.Tbl.mem self.m t); - T.Tbl.add self.m t v; - List.iter (fun u -> require_eval self u) subs; - () + if not @@ T.Tbl.mem self.m t then ( + T.Tbl.add self.m t v; + List.iter (fun u -> require_eval self u) subs + ) type eval_cache = Term.Internal_.cache