From 06a999e219ed599c2c57cf9df7b7ee71747f7e79 Mon Sep 17 00:00:00 2001
From: Jakob Rath <git@jakobrath.eu>
Date: Thu, 15 Dec 2022 13:46:10 +0100
Subject: [PATCH] skip diseq when not using polysat

---
 src/sat/smt/bv_polysat.cpp | 2 ++
 1 file changed, 2 insertions(+)

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);