From e58b29da02cd2ed769c3ff808afe24ccda340796 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Sat, 28 Dec 2019 08:49:14 -0600 Subject: [PATCH] fix(term): hashconsing error leading to non termination --- src/base-term/Base_types.ml | 2 ++ src/msat-solver/Sidekick_msat_solver.ml | 1 + src/smtlib/Process.ml | 2 +- 3 files changed, 4 insertions(+), 1 deletion(-) diff --git a/src/base-term/Base_types.ml b/src/base-term/Base_types.ml index c139a3db..2e745b5b 100644 --- a/src/base-term/Base_types.ml +++ b/src/base-term/Base_types.ml @@ -549,6 +549,8 @@ end = struct Fun.equal f1 f2 && IArray.equal sub_eq a1 a2 | Eq(a1,b1), Eq(a2,b2) -> sub_eq a1 a2 && sub_eq b1 b2 | Not a, Not b -> sub_eq a b + | Ite (a1,b1,c1), Ite (a2,b2,c2) -> + sub_eq a1 a2 && sub_eq b1 b2 && sub_eq c1 c2 | (Bool _ | App_fun _ | Eq _ | Not _ | Ite _), _ -> false diff --git a/src/msat-solver/Sidekick_msat_solver.ml b/src/msat-solver/Sidekick_msat_solver.ml index fc3de178..ce2fdc6f 100644 --- a/src/msat-solver/Sidekick_msat_solver.ml +++ b/src/msat-solver/Sidekick_msat_solver.ml @@ -558,6 +558,7 @@ module Make(A : ARG) let add_clause (self:t) (c:Atom.t IArray.t) : unit = Stat.incr self.count_clause; + Log.debugf 50 (fun k->k "add clause %a@." (Util.pp_iarray Atom.pp) c); Sat_solver.add_clause_a self.solver (c:> Atom.t array) P.default let add_clause_l self c = add_clause self (IArray.of_list c) diff --git a/src/smtlib/Process.ml b/src/smtlib/Process.ml index 00899d0b..8765976f 100644 --- a/src/smtlib/Process.ml +++ b/src/smtlib/Process.ml @@ -200,7 +200,7 @@ let process_stmt (solver:Solver.t) (stmt:Statement.t) : unit or_error = Log.debugf 5 - (fun k->k "(@[<2>process statement@ %a@])" Statement.pp stmt); + (fun k->k "(@[smtlib.process-statement@ %a@])" Statement.pp stmt); let decl_sort c n : unit = Log.debugf 1 (fun k->k "(@[declare-sort %a@ :arity %d@])" ID.pp c n); (* TODO: more? *)