From c2f9d35d59094c9d7da81f4b63864d199283724f Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 29 Jun 2016 16:53:28 -0700
Subject: [PATCH] throw exceptions when internalizing expressions with free
 variables, issue #663

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/smt/smt_internalizer.cpp |  6 +++---
 src/smt/theory_arith_core.h  | 22 ++++++++++++++++++----
 2 files changed, 21 insertions(+), 7 deletions(-)

diff --git a/src/smt/smt_internalizer.cpp b/src/smt/smt_internalizer.cpp
index df80d3281..45bd75ab7 100644
--- a/src/smt/smt_internalizer.cpp
+++ b/src/smt/smt_internalizer.cpp
@@ -321,10 +321,10 @@ namespace smt {
     void context::internalize(expr * n, bool gate_ctx) {
         TRACE("internalize", tout << "internalizing:\n" << mk_pp(n, m_manager) << "\n";);
         TRACE("internalize_bug", tout << "internalizing:\n" << mk_bounded_pp(n, m_manager) << "\n";);
+        if (is_var(n)) {
+            throw default_exception("Formulas should not contain unbound variables");
+        }
         if (m_manager.is_bool(n)) {
-            if (is_var(n)) {
-                throw default_exception("Formulas should not contain unbound variables");
-            }
             SASSERT(is_quantifier(n) || is_app(n));
             internalize_formula(n, gate_ctx);
         }
diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h
index 8dfe8498f..8e7765ee9 100644
--- a/src/smt/theory_arith_core.h
+++ b/src/smt/theory_arith_core.h
@@ -268,7 +268,7 @@ namespace smt {
         }
         rational _val; 
         expr* arg1, *arg2;
-        if (m_util.is_mul(m, arg1, arg2) && m_util.is_numeral(arg1, _val)) {
+        if (m_util.is_mul(m, arg1, arg2) && m_util.is_numeral(arg1, _val) && is_app(arg1) && is_app(arg2)) {
             SASSERT(m->get_num_args() == 2);
             numeral val(_val);
             theory_var v = internalize_term_core(to_app(arg2));
@@ -297,6 +297,11 @@ namespace smt {
         scoped_row_vars _sc(m_row_vars, m_row_vars_top);
         unsigned num_args = n->get_num_args();
         for (unsigned i = 0; i < num_args; i++) {
+            if (is_var(n->get_arg(i))) {
+                std::ostringstream strm;
+                strm << mk_pp(n, get_manager()) << " contains a free variable";
+                throw default_exception(strm.str());
+            }
             internalize_internal_monomial(to_app(n->get_arg(i)), r_id);
         }
         enode * e = mk_enode(n);
@@ -356,6 +361,11 @@ namespace smt {
             SASSERT(!val.is_one());
             unsigned r_id = mk_row();
             scoped_row_vars _sc(m_row_vars, m_row_vars_top);
+            if (is_var(m->get_arg(1))) {
+                std::ostringstream strm;
+                strm << mk_pp(m, get_manager()) << " contains a free variable";
+                throw default_exception(strm.str());
+            }
             if (reflection_enabled())
                 internalize_term_core(to_app(m->get_arg(0)));
             theory_var v = internalize_mul_core(to_app(m->get_arg(1)));
@@ -1204,6 +1214,9 @@ namespace smt {
             kind = A_UPPER;
         else
             kind = A_LOWER;
+        if (!is_app(n->get_arg(0)) || !is_app(n->get_arg(1))) {
+            return false;
+        }
         app * lhs      = to_app(n->get_arg(0));
         app * rhs      = to_app(n->get_arg(1));
         expr * rhs2;
@@ -1245,10 +1258,11 @@ namespace smt {
 
     template<typename Ext>
     void theory_arith<Ext>::internalize_eq_eh(app * atom, bool_var v) {
-        if (m_params.m_arith_eager_eq_axioms) {
+        expr* _lhs, *_rhs;
+        if (m_params.m_arith_eager_eq_axioms && get_manager().is_eq(atom, _lhs, _rhs) && is_app(_lhs) && is_app(_rhs)) {
             context & ctx  = get_context();
-            app * lhs      = to_app(atom->get_arg(0));
-            app * rhs      = to_app(atom->get_arg(1));
+            app * lhs      = to_app(_lhs);
+            app * rhs      = to_app(_rhs);
             enode * n1 = ctx.get_enode(lhs);
             enode * n2 = ctx.get_enode(rhs);
             // The expression atom may be a theory axiom. In this case, it may not be in simplified form.