From 3ce0e900ff56f03b06484f64e9ae723e4feecb79 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 18 Nov 2012 18:31:35 -0800
Subject: [PATCH] register also head predicate

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/muz_qe/pdr_tactic.cpp | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/muz_qe/pdr_tactic.cpp b/src/muz_qe/pdr_tactic.cpp
index 6b1b13e67..6bf9e8ed1 100644
--- a/src/muz_qe/pdr_tactic.cpp
+++ b/src/muz_qe/pdr_tactic.cpp
@@ -174,6 +174,7 @@ class pdr_tactic : public tactic {
 
             if (queries.size() != 1) {
                 q = m.mk_fresh_const("query", m.mk_bool_sort());
+                register_predicate(q);
                 for (unsigned i = 0; i < queries.size(); ++i) {
                     f = mk_rule(queries[i].get(), q);
                     m_ctx.add_rule(f, symbol::null);