diff --git a/src/smt/smt_model_finder.cpp b/src/smt/smt_model_finder.cpp
index 6ef1e55c6e..1dc63ff2a4 100644
--- a/src/smt/smt_model_finder.cpp
+++ b/src/smt/smt_model_finder.cpp
@@ -1413,8 +1413,6 @@ namespace smt {
                 // add other possible relevant functions such as equality over srt, Boolean operators
 
                 ast_mark visited;
-                tn.add_production(m.mk_true());
-                tn.add_production(m.mk_false());
                 for (enode *n : ctx->enodes()) {
                     if (!ctx->is_relevant(n))
                         continue;