From 00e8ea79621c5029d6773e3164ded601161c0898 Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Tue, 14 Sep 2021 15:46:58 +0000
Subject: [PATCH] Make terms that are internalized on the fly relevant

---
 src/smt/theory_fpa.cpp | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

diff --git a/src/smt/theory_fpa.cpp b/src/smt/theory_fpa.cpp
index c36346de400..d1f60eb973b 100644
--- a/src/smt/theory_fpa.cpp
+++ b/src/smt/theory_fpa.cpp
@@ -38,7 +38,7 @@ namespace smt {
     {
         params_ref p;
         p.set_bool("arith_lhs", true);
-        m_th_rw.updt_params(p);        
+        m_th_rw.updt_params(p);
     }
 
     theory_fpa::~theory_fpa()
@@ -284,6 +284,9 @@ namespace smt {
             }
             default: /* ignore */;
             }
+
+            if (!ctx.relevancy())
+                relevant_eh(term);
         }
 
         return true;
@@ -623,7 +626,7 @@ namespace smt {
         bv2fp.convert_min_max_specials(&mdl, &new_model, seen);
         bv2fp.convert_uf2bvuf(&mdl, &new_model, seen);
 
-        for (func_decl* f : seen) 
+        for (func_decl* f : seen)
             mdl.unregister_decl(f);
 
         for (unsigned i = 0; i < new_model.get_num_constants(); i++) {