From d7b82366c633075ac1754d63931fa19fdd4dd614 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 11 Oct 2024 19:33:39 -0700
Subject: [PATCH] avoid units

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/sls/sls_euf_plugin.cpp | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/ast/sls/sls_euf_plugin.cpp b/src/ast/sls/sls_euf_plugin.cpp
index 97de59283..5a26c0651 100644
--- a/src/ast/sls/sls_euf_plugin.cpp
+++ b/src/ast/sls/sls_euf_plugin.cpp
@@ -98,6 +98,8 @@ namespace sls {
             sat::literal l = to_literal(p);
             SASSERT(ctx.is_true(l));
             lits.push_back(~l);
+            if (ctx.is_unit(l))
+                continue;
             if (ctx.rand(++n) == 0)
                 flit = l;
         }