diff --git a/src/sat/smt/bv_polysat.cpp b/src/sat/smt/bv_polysat.cpp
index 77e170e77..1345dde6a 100644
--- a/src/sat/smt/bv_polysat.cpp
+++ b/src/sat/smt/bv_polysat.cpp
@@ -218,6 +218,8 @@ namespace bv {
     }
 
     bool solver::polysat_diseq_eh(euf::th_eq const& ne) {
+        if (!use_polysat())
+            return false;
         euf::theory_var v1 = ne.v1(), v2 = ne.v2();
         pdd p = var2pdd(v1);
         pdd q = var2pdd(v2);