From 0949ad26c2f802d543612ed8edb344484a836fdb Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 16 Mar 2021 15:24:34 -0700
Subject: [PATCH] fix #5107

---
 src/test/model_evaluator.cpp | 2 --
 1 file changed, 2 deletions(-)

diff --git a/src/test/model_evaluator.cpp b/src/test/model_evaluator.cpp
index 68a24e792..3e1c95617 100644
--- a/src/test/model_evaluator.cpp
+++ b/src/test/model_evaluator.cpp
@@ -60,8 +60,6 @@ void tst_model_evaluator() {
     {
         fi->set_else(m.mk_app(F, vI0p, vB1p));
         gi->set_else(m.mk_app(G, vI0p, vB1p));
-        mdl.register_decl(g, gi);
-        mdl.register_decl(h, hi);
         model_pp(std::cout, mdl);
         e = m.mk_app(h, vI0p, vB1p);
         eval(e, v);