From af9ae3598439d9027b1cffe0f233457e877825fa Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 20 Jan 2022 14:43:16 +0100
Subject: [PATCH] term

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/smt/theory_user_propagator.cpp | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/smt/theory_user_propagator.cpp b/src/smt/theory_user_propagator.cpp
index 10820de3b..06422cbf0 100644
--- a/src/smt/theory_user_propagator.cpp
+++ b/src/smt/theory_user_propagator.cpp
@@ -59,6 +59,7 @@ unsigned theory_user_propagator::add_expr(expr* e) {
         ctx.set_var_theory(bv, get_id());
         ctx.set_enode_flag(bv, true);
     }
+    SASSERT(!m.is_bool(e) || ctx.b_internalized(e));
 
     ctx.attach_th_var(n, this, v);
     literal_vector explain;