simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-05 19:00:33 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

fix(lra): preprocess was returning wrong term

Browse source 
(with wrong type).
This commit is contained in:
Simon Cruanes 2022-09-11 14:36:38 -04:00
parent 469b97934a
commit c18b824037
No known key found for this signature in database
GPG key ID: EBFFF6F283F3A2B4
1 changed files with 1 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/th-lra/sidekick_th_lra.ml
View file

@ -310,10 +310,6 @@ module Make (A : ARG) = (* : S with module A = A *) struct
in in
match A.view_as_lra t with 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 | LRA_pred (((Eq | Neq) as pred), t1, t2) when is_const_ t1 && is_const_ t2
-> ->
(* comparison of constants: can decide right now *) (* 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; Term.Tbl.add self.encoded_lits box_t box_t;
Log.debugf 50 (fun k -> 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); SimpSolver.Constraint.pp constr);
Some box_t Some box_t