#5336

Z3Prover · Jun 9, 2021 · 082ec0f · 082ec0f
1 parent 08b4c4e
commit 082ec0f
Showing 1 changed file with 1 addition and 1 deletion.
diff --git 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;