From 570f2bd8e5d5181cef7e5b4321f66725c34c3b36 Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Tue, 2 Feb 2021 04:35:25 -0800 Subject: [PATCH] [sledge] Improve test in Context.propagate1 Summary: Currently `not Theory.is_interpreted` is used to terms should be added to classes, or delayed to pending equations. This diff changes this to use `Theory.is_noninterpreted` instead. They only differ on `Z _ | Q _ | Concat [||]`, which do not make it to this test, and `is_noninterpreted` is more correct since classes may only contain solvables. Reviewed By: jvillard Differential Revision: D25883706 fbshipit-source-id: 3b7b94065 --- sledge/src/fol/context.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/sledge/src/fol/context.ml b/sledge/src/fol/context.ml index c59d8c2ad..a0c67b636 100644 --- a/sledge/src/fol/context.ml +++ b/sledge/src/fol/context.ml @@ -448,8 +448,8 @@ let propagate1 (a, a') x = |> Option.value ~default:(Cls.empty, x.cls) in let b0'_cls, pnd = - if Theory.is_interpreted b0' then (b0'_cls, (b0', b') :: x.pnd) - else (Cls.add b0' b0'_cls, x.pnd) + if Theory.is_noninterpreted b0' then (Cls.add b0' b0'_cls, x.pnd) + else (b0'_cls, (b0', b') :: x.pnd) in let rep = Cls.fold b0'_cls x.rep ~f:(fun c rep ->