From ecf9c629b044c7fa8cf0ca40cdec9a144285dbf7 Mon Sep 17 00:00:00 2001
From: Arie Gurfinkel <arie.gurfinkel@uwaterloo.ca>
Date: Tue, 26 Dec 2017 16:48:37 -0500
Subject: [PATCH] Fix binding handling for quantifier free lemmas

---
 src/muz/spacer/spacer_context.cpp | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/muz/spacer/spacer_context.cpp b/src/muz/spacer/spacer_context.cpp
index c7f9f448f..1151909f1 100644
--- a/src/muz/spacer/spacer_context.cpp
+++ b/src/muz/spacer/spacer_context.cpp
@@ -1307,6 +1307,8 @@ bool lemma::has_binding(app_ref_vector const &binding) {
 
     SASSERT(binding.size() == num_decls);
 
+    if (num_decls == 0) return true;
+
     for (unsigned off = 0, sz = m_bindings.size(); off < sz; off += num_decls) {
         unsigned i = 0;
         for (; i < num_decls; ++i) {