From 008fc648c15cafb7561c3c089d828e62c9d4c677 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 25 Nov 2012 16:53:13 -0800
Subject: [PATCH] ensure there are enough variables

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

diff --git a/src/muz_qe/dl_context.cpp b/src/muz_qe/dl_context.cpp
index 12c12c75a..f38999381 100644
--- a/src/muz_qe/dl_context.cpp
+++ b/src/muz_qe/dl_context.cpp
@@ -338,7 +338,7 @@ namespace datalog {
 
     expr_ref context::bind_variables(expr* fml, bool is_forall) {
         expr_ref result(m);
-        app_ref_vector const& vars = m_vars;
+        app_ref_vector & vars = m_vars;
         if (vars.empty()) {
             result = fml;
         }
@@ -352,6 +352,9 @@ namespace datalog {
             else {
                 svector<symbol> names;
                 for (unsigned i = 0; i < sorts.size(); ++i) {
+                    if (vars.size() == i) {
+                        vars.push_back(m.mk_fresh_const("x", m.mk_bool_sort()));
+                    }
                     if (!sorts[i]) {
                         sorts[i] = vars[i]->get_decl()->get_range();
                     }