From 5db84575f6d1d57094283d9b473020e720735e4f Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 8 Mar 2016 22:27:47 -0800
Subject: [PATCH] fix regression in o7.smt2

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/opt/opt_context.cpp | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp
index 307dbfda4..6495b11ec 100644
--- a/src/opt/opt_context.cpp
+++ b/src/opt/opt_context.cpp
@@ -896,7 +896,7 @@ namespace opt {
                 }
                 mk_atomic(terms);
                 SASSERT(obj.m_id == id);
-                obj.m_term = to_app(orig_term);
+                obj.m_term = orig_term?to_app(orig_term):0;
                 obj.m_terms.reset();
                 obj.m_terms.append(terms);
                 obj.m_weights.reset();
@@ -940,6 +940,9 @@ namespace opt {
     bool context::verify_model(unsigned index, model* md, rational const& _v) {
         rational r;
         app_ref term = m_objectives[index].m_term;
+        if (!term) {
+            return true;
+        }
         rational v = m_objectives[index].m_adjust_value(_v);
         expr_ref val(m);
         model_ref mdl = md;