mirror of
https://github.com/Z3Prover/z3
synced 2025-04-06 17:44:08 +00:00
#7353 - clear pointer when existing stack
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
c1454dc31c
commit
6a68cc55bb
|
@ -613,7 +613,7 @@ namespace sat {
|
|||
out << ci.m_num_trues << " " << ci.m_weight << "\n";
|
||||
}
|
||||
for (unsigned v = 0; v < num_vars(); ++v) {
|
||||
out << v << ": " << reward(v) << "\n";
|
||||
out << v << ": rw " << reward(v) << "\n";
|
||||
}
|
||||
out << "unsat vars: ";
|
||||
for (bool_var v : m_unsat_vars) {
|
||||
|
|
|
@ -35,7 +35,7 @@ class fix_dl_var_tactic : public tactic {
|
|||
struct failed {};
|
||||
ast_manager & m;
|
||||
arith_util & m_util;
|
||||
expr_fast_mark1 * m_visited;
|
||||
expr_fast_mark1 * m_visited = nullptr;
|
||||
ptr_vector<expr> m_todo;
|
||||
obj_map<app, unsigned> m_occs;
|
||||
obj_map<app, unsigned> m_non_nested_occs;
|
||||
|
@ -215,7 +215,7 @@ class fix_dl_var_tactic : public tactic {
|
|||
app * operator()(goal const & g) {
|
||||
try {
|
||||
expr_fast_mark1 visited;
|
||||
m_visited = &visited;
|
||||
flet<expr_fast_mark1*> _visited(m_visited, &visited);
|
||||
unsigned sz = g.size();
|
||||
for (unsigned i = 0; i < sz; i++) {
|
||||
process(g.form(i));
|
||||
|
|
Loading…
Reference in a new issue