From 082ec0f49988712c683b1737356e27f2d6416455 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 8 Jun 2021 20:03:03 -0700
Subject: [PATCH] #5336

---
 src/sat/smt/q_solver.h | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/sat/smt/q_solver.h b/src/sat/smt/q_solver.h
index 9b0301775..426104c87 100644
--- a/src/sat/smt/q_solver.h
+++ b/src/sat/smt/q_solver.h
@@ -74,7 +74,7 @@ namespace q {
         euf::th_solver* clone(euf::solver& ctx) override;
         bool unit_propagate() override;
         sat::literal internalize(expr* e, bool sign, bool root, bool learned) override;
-        void internalize(expr* e, bool redundant) override { UNREACHABLE(); }
+        void internalize(expr* e, bool redundant) override { internalize(e, false, false, redundant); }
         euf::theory_var mk_var(euf::enode* n) override;
         void init_search() override;
         void finalize_model(model& mdl) override;