diff --git a/src/math/lp/gomory.cpp b/src/math/lp/gomory.cpp
index 5148dedc0..46f745d03 100644
--- a/src/math/lp/gomory.cpp
+++ b/src/math/lp/gomory.cpp
@@ -298,7 +298,7 @@ public:
             mpq t = abs(ceil(p.coeff()));
             if (t > m_abs_max) m_abs_max = t;
         }
-        m_big_number = m_abs_max; // .expt(2);
+        m_big_number = m_abs_max.expt(2);
 #endif
         mpq one_min_m_f = 1 - m_f;
         for (const auto & p : m_row) {
diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp
index 596179145..bf807dc6e 100644
--- a/src/sat/tactic/goal2sat.cpp
+++ b/src/sat/tactic/goal2sat.cpp
@@ -142,6 +142,11 @@ struct goal2sat::imp {
             else if (m.is_false(t)) {
                 l = sign ? mk_true() : ~mk_true();
             }
+            else if (!is_app(t)) {
+                std::ostringstream strm;
+                strm << mk_ismt2_pp(t, m);
+                throw_op_not_handled(strm.str());
+            }
             else {
                 bool ext = m_default_external || !is_uninterp_const(t) || m_interface_vars.contains(t);
                 sat::bool_var v = m_solver.add_var(ext);