From 3d0461936f31446b3a57ddb0f99c7dd1da798ee6 Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Sun, 11 Sep 2022 14:10:01 -0400
Subject: [PATCH] fix: remove spurious check?

---
 src/smt/preprocess.ml | 1 -
 1 file changed, 1 deletion(-)

diff --git a/src/smt/preprocess.ml b/src/smt/preprocess.ml
index a2537d6c..9775662b 100644
--- a/src/smt/preprocess.ml
+++ b/src/smt/preprocess.ml
@@ -61,7 +61,6 @@ let preprocess_term_ (self : t) acts (t : term) : term =
           (* only accept a box (with possible side effect: new clauses, etc.) *)
           Log.debugf 20 (fun k ->
               k "(@[smt.preprocess.tr@ %a@ :into %a@])" Term.pp t0 Term.pp u);
-          assert (Box.is_box u || Term.is_const u);
           u
         | None ->
           (* just preprocess subterms *)