From 4dcc3ea4ada766aec3988f5859bcaebe0d996111 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Sun, 7 Aug 2022 22:41:13 -0400 Subject: [PATCH] small changes in smt --- src/smt/solver.ml | 4 ++-- src/smt/solver_internal.ml | 8 ++++---- 2 files changed, 6 insertions(+), 6 deletions(-) diff --git a/src/smt/solver.ml b/src/smt/solver.ml index fb71706c..6f92f526 100644 --- a/src/smt/solver.ml +++ b/src/smt/solver.ml @@ -103,8 +103,8 @@ let create arg ?(stat = Stat.global) ?size ~proof ~theories tst () : t = last_res = None; solver = Sat_solver.create ~proof ?size ~stat (SI.to_sat_plugin si); stat; - count_clause = Stat.mk_int stat "solver.add-clause"; - count_solve = Stat.mk_int stat "solver.solve"; + count_clause = Stat.mk_int stat "smt.solver.add-clause"; + count_solve = Stat.mk_int stat "smt.solver.solve"; } in add_theory_l self theories; diff --git a/src/smt/solver_internal.ml b/src/smt/solver_internal.ml index e6e73bb9..eff96801 100644 --- a/src/smt/solver_internal.ml +++ b/src/smt/solver_internal.ml @@ -607,10 +607,10 @@ let create (module A : ARG) ~stat ~proof (tst : Term.store) () : t = registry = Registry.create (); preprocessed = Term.Tbl.create 32; delayed_actions = Queue.create (); - count_axiom = Stat.mk_int stat "solver.th-axioms"; - count_preprocess_clause = Stat.mk_int stat "solver.preprocess-clause"; - count_propagate = Stat.mk_int stat "solver.th-propagations"; - count_conflict = Stat.mk_int stat "solver.th-conflicts"; + count_axiom = Stat.mk_int stat "smt.solver.th-axioms"; + count_preprocess_clause = Stat.mk_int stat "smt.solver.preprocess-clause"; + count_propagate = Stat.mk_int stat "smt.solver.th-propagations"; + count_conflict = Stat.mk_int stat "smt.solver.th-conflicts"; on_partial_check = []; on_final_check = []; on_th_combination = [];