From c18b82403741d268f4512d0724dfe1d0f62d299e Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Sun, 11 Sep 2022 14:36:38 -0400 Subject: [PATCH] fix(lra): preprocess was returning wrong term (with wrong type). --- src/th-lra/sidekick_th_lra.ml | 6 +----- 1 file changed, 1 insertion(+), 5 deletions(-) diff --git a/src/th-lra/sidekick_th_lra.ml b/src/th-lra/sidekick_th_lra.ml index 18351c82..5bd8a353 100644 --- a/src/th-lra/sidekick_th_lra.ml +++ b/src/th-lra/sidekick_th_lra.ml @@ -310,10 +310,6 @@ module Make (A : ARG) = (* : S with module A = A *) struct in match A.view_as_lra t with - | _ when Term.Tbl.mem self.simp_preds t -> - let u, _, _ = Term.Tbl.find self.simp_preds t in - Some u - (* already turned into a simplex predicate *) | LRA_pred (((Eq | Neq) as pred), t1, t2) when is_const_ t1 && is_const_ t2 -> (* comparison of constants: can decide right now *) @@ -390,7 +386,7 @@ module Make (A : ARG) = (* : S with module A = A *) struct Term.Tbl.add self.encoded_lits box_t box_t; Log.debugf 50 (fun k -> - k "(@[lra.preproc@ :t %a@ :to-constr %a@])" Term.pp t + k "(@[lra.preprocess.pred@ :t %a@ :to-constr %a@])" Term.pp t SimpSolver.Constraint.pp constr); Some box_t