diff --git a/src/ast/sls/sls_euf_plugin.cpp b/src/ast/sls/sls_euf_plugin.cpp
index 8ab5f73df..ff1a72748 100644
--- a/src/ast/sls/sls_euf_plugin.cpp
+++ b/src/ast/sls/sls_euf_plugin.cpp
@@ -287,34 +287,35 @@ namespace sls {
                 if (m.is_eq(e)) {
                     a = g.find(to_app(e)->get_arg(0));
                     b = g.find(to_app(e)->get_arg(1));
-                }
-                if (lit.sign() && m.is_eq(e)) {
-                    if (a && b && a->get_root() == b->get_root()) {
-                        IF_VERBOSE(0, verbose_stream() << "not disequal " << lit << " " << mk_pp(e, m) << "\n");
-                        ctx.display(verbose_stream());
-                        UNREACHABLE();
+                    if (lit.sign()) {
+                        if (a && b && a->get_root() == b->get_root()) {
+                            IF_VERBOSE(0, verbose_stream() << "not disequal " << lit << " " << mk_pp(e, m) << "\n");
+                            ctx.display(verbose_stream());
+                            UNREACHABLE();
+                        }
+                    }
+                    else {
+                        if (a && b && a->get_root() != b->get_root()) {
+                            IF_VERBOSE(0, verbose_stream() << "not equal " << lit << " " << mk_pp(e, m) << "\n");
+                            //UNREACHABLE();
+                        }
                     }
                 }
-                else if (!lit.sign() && m.is_eq(e)) {
-                    if (a && b && a->get_root() != b->get_root()) {
-                        IF_VERBOSE(0, verbose_stream() << "not equal " << lit << " " << mk_pp(e, m) << "\n");
-                        //UNREACHABLE();
-                    }
-                }
-                else if (to_app(e)->get_family_id() != basic_family_id && lit.sign()) {
+                else if (to_app(e)->get_family_id() != basic_family_id) {
                     auto* ne = g.find(e);
-                    auto* nf = g.find(m.mk_false());
-                    if (ne && nf && ne->get_root() != nf->get_root()) {
-                        IF_VERBOSE(0, verbose_stream() << "not false " << lit << " " << mk_pp(e, m) << "\n");
-                        //UNREACHABLE();
+                    if (lit.sign()) {
+                        auto* nf = g.find(m.mk_false());
+                        if (ne && nf && ne->get_root() != nf->get_root()) {
+                            IF_VERBOSE(0, verbose_stream() << "not false " << lit << " " << mk_pp(e, m) << "\n");
+                            //UNREACHABLE();
+                        }
                     }
-                }
-                else if (to_app(e)->get_family_id() != basic_family_id && !lit.sign()) {
-                    auto* ne = g.find(e);
-                    auto* nt = g.find(m.mk_true());
-                    if (ne && nt && ne->get_root() != nt->get_root()) {
-                        IF_VERBOSE(0, verbose_stream() << "not true " << lit << " " << mk_pp(e, m) << "\n");
-                        //UNREACHABLE();
+                    else {
+                        auto* nt = g.find(m.mk_true());
+                        if (ne && nt && ne->get_root() != nt->get_root()) {
+                            IF_VERBOSE(0, verbose_stream() << "not true " << lit << " " << mk_pp(e, m) << "\n");
+                            //UNREACHABLE();
+                        }
                     }
                 }
             
diff --git a/src/math/realclosure/realclosure.cpp b/src/math/realclosure/realclosure.cpp
index 8b11e1725..4ba1c11fa 100644
--- a/src/math/realclosure/realclosure.cpp
+++ b/src/math/realclosure/realclosure.cpp
@@ -3448,16 +3448,21 @@ namespace realclosure {
             return true;
         }
 
-        unsigned get_sign_condition_size(numeral const &a, unsigned i) {
-            algebraic * ext = to_algebraic(to_rational_function(a)->ext());
+        sign_condition* get_ith_sign_condition(algebraic* ext, unsigned i) {
             const sign_det * sdt = ext->sdt();
             if (!sdt)
-                return 0;
+                return nullptr;
             sign_condition * sc = sdt->sc(ext->sc_idx());
-            while (i) {
-                if (sc) sc = sc->prev();
+            while (i && sc) {
+                sc = sc->prev();
                 i--;
             }
+            return sc;
+        }
+
+        unsigned get_sign_condition_size(numeral const &a, unsigned i) {
+            algebraic * ext = to_algebraic(to_rational_function(a)->ext());
+            sign_condition * sc = get_ith_sign_condition(ext, i);
             if (!sc)
                 return 0;
             return ext->sdt()->qs()[sc->qidx()].size();
@@ -3468,14 +3473,7 @@ namespace realclosure {
             if (!is_algebraic(a))
                 return 0;
             algebraic * ext = to_algebraic(to_rational_function(a)->ext());
-            const sign_det * sdt = ext->sdt();
-            if (!sdt)
-                return 0;
-            sign_condition * sc = sdt->sc(ext->sc_idx());
-            while (i) {
-                if (sc) sc = sc->prev();
-                i--;
-            }
+            sign_condition * sc = get_ith_sign_condition(ext, i);
             if (!sc)
                 return 0;
             const polynomial & q = ext->sdt()->qs()[sc->qidx()];
@@ -3487,14 +3485,7 @@ namespace realclosure {
             if (!is_algebraic(a))
                 return numeral();
             algebraic * ext = to_algebraic(to_rational_function(a)->ext());
-            const sign_det * sdt = ext->sdt();
-            if (!sdt)
-                return numeral();
-            sign_condition * sc = sdt->sc(ext->sc_idx());
-            while (i) {
-                if (sc) sc = sc->prev();
-                i--;
-            }
+            sign_condition * sc = get_ith_sign_condition(ext, i);
             if (!sc)
                 return numeral();
             const polynomial & q = ext->sdt()->qs()[sc->qidx()];