From fbf8289394f4e4d78ef9c360e4b4b47d9bd961b4 Mon Sep 17 00:00:00 2001
From: nikolajbjorner <nbjorner@microsoft.com>
Date: Tue, 24 Feb 2015 14:02:23 -0800
Subject: [PATCH] probe also hard constraints before enabling SAT solver. Bug
 reported by Zvonimir Pavlinovic

Signed-off-by: nikolajbjorner <nbjorner@microsoft.com>
---
 src/opt/opt_context.cpp | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp
index f22ce479e..b98343013 100644
--- a/src/opt/opt_context.cpp
+++ b/src/opt/opt_context.cpp
@@ -533,6 +533,9 @@ namespace opt {
             for (unsigned i = 0; i < sz; i++) {
                 quick_for_each_expr(proc, visited, get_solver().get_assertion(i));
             }
+            for (unsigned i = 0; i < m_hard_constraints.size(); ++i) {
+                quick_for_each_expr(proc, visited, m_hard_constraints[i].get());
+            }
         }
         catch (is_bv::found) {
             return false;