mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-19 19:02:02 +00:00
Code Activity

minor fixes to rel_context

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2013-04-10 20:06:21 -07:00
parent 312e052788
commit cdb90968e3
1 changed files with 3 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/muz_qe/rel_context.cpp
View file

@ -40,7 +40,9 @@ namespace datalog {
rule_set m_rules; rule_set m_rules;
decl_set m_preds; decl_set m_preds;
bool m_was_closed; bool m_was_closed;
public: public:
scoped_query(context& ctx): scoped_query(context& ctx):
m_ctx(ctx), m_ctx(ctx),
m_rules(ctx.get_rules()), m_rules(ctx.get_rules()),
@ -51,6 +53,7 @@ namespace datalog {
ctx.reopen(); ctx.reopen();
} }
} }
~scoped_query() { ~scoped_query() {
m_ctx.reopen(); m_ctx.reopen();
m_ctx.restrict_predicates(m_preds); m_ctx.restrict_predicates(m_preds);
@ -235,7 +238,6 @@ namespace datalog {
query_pred = rm.mk_query(query, m_context.get_rules()); query_pred = rm.mk_query(query, m_context.get_rules());
} }
catch (default_exception& exn) { catch (default_exception& exn) {
m_context.close();
m_context.set_status(INPUT_ERROR); m_context.set_status(INPUT_ERROR);
throw exn; throw exn;
} }