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