From 7806a446f63ae57a7f91e84d7d4c4a72d65ddf05 Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Tue, 2 Feb 2021 04:35:33 -0800 Subject: [PATCH] [sledge] Tighten test for uninterp terms in Context.solve_uninterp_eqs Summary: Context.solve_uninterp_eqs uses `not Theory.is_interpreted` where `Theory.is_noninterpreted` is more correct, since it operates on terms that are class elements, which cannot be `Z _ | Q _ | Concat [||]`. Reviewed By: jvillard Differential Revision: D25883732 fbshipit-source-id: 5d060b338 --- sledge/src/fol/context.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/sledge/src/fol/context.ml b/sledge/src/fol/context.ml index a0c67b636..cdf19f694 100644 --- a/sledge/src/fol/context.ml +++ b/sledge/src/fol/context.ml @@ -995,7 +995,7 @@ type cls_solve_state = let dom_trm e = match (e : Trm.t) with | Sized {seq= Var _ as v} -> Some v - | _ when not (Theory.is_interpreted e) -> Some e + | _ when Theory.is_noninterpreted e -> Some e | _ -> None (** move equations from [cls] (which is assumed to be normalized by [subst])