From f5ccbb476b2693e1259e3071c137d2983c781deb Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Sun, 23 Oct 2022 20:58:25 -0400 Subject: [PATCH] add todo --- src/smtlib/Driver.ml | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/smtlib/Driver.ml b/src/smtlib/Driver.ml index 0a8c4ecb..9a572b91 100644 --- a/src/smtlib/Driver.ml +++ b/src/smtlib/Driver.ml @@ -69,7 +69,10 @@ let decl_fun (self : t) f args ret const : unit = let build_model (self : t) (sat : Solver.sat_result) : Model.t = Build_model.build self.build_model sat -let check_model (self : t) (m : Model.t) : unit = assert false +(* FIXME *) +let check_model (_self : t) (_m : Model.t) : unit = + Log.debugf 0 (fun k -> k "; TODO: check model"); + () (* call the solver to check satisfiability *) let solve (self : t) ~assumptions () : Solver.res =