From b9f6fc5130b9292f569742fb0dd3d14b26874b3d Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 30 Jun 2021 13:55:57 -0700
Subject: [PATCH] debug buidl

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/math/dd/dd_bdd.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/math/dd/dd_bdd.cpp b/src/math/dd/dd_bdd.cpp
index 20f95bd5c..402b47a45 100644
--- a/src/math/dd/dd_bdd.cpp
+++ b/src/math/dd/dd_bdd.cpp
@@ -582,7 +582,7 @@ namespace dd {
     bdd bdd_manager::mk_cofactor(bdd const& a, bdd const& b) {
 	bool first = true;
         scoped_push _sp(*this);
-	    SASSERT(!is_const(b) && is_const(lo(b)) && is_const(hi(b)));
+        SASSERT(!b.is_const() && b.lo().is_const() && b.hi().is_const());
         while (true) {
             try {
                 return bdd(mk_cofactor_rec(a.root, b.root), this);