mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 14:13:23 +00:00
Code Activity

register also head predicate

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2012-11-18 18:31:35 -08:00
parent 3dbf617a46
commit 3ce0e900ff
1 changed files with 1 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/muz_qe/pdr_tactic.cpp
View file

@ -174,6 +174,7 @@ class pdr_tactic : public tactic {
if (queries.size() != 1) { if (queries.size() != 1) {
q = m.mk_fresh_const("query", m.mk_bool_sort()); q = m.mk_fresh_const("query", m.mk_bool_sort());
register_predicate(q);
for (unsigned i = 0; i < queries.size(); ++i) { for (unsigned i = 0; i < queries.size(); ++i) {
f = mk_rule(queries[i].get(), q); f = mk_rule(queries[i].get(), q);
m_ctx.add_rule(f, symbol::null); m_ctx.add_rule(f, symbol::null);