mirror of
https://github.com/Z3Prover/z3
synced 2025-04-12 12:08:18 +00:00
This commit is contained in:
parent
496ec5f2b4
commit
178262fc12
|
@ -235,7 +235,7 @@ namespace euf {
|
||||||
enode* find(expr* f, unsigned n, enode* const* args);
|
enode* find(expr* f, unsigned n, enode* const* args);
|
||||||
enode* mk(expr* f, unsigned generation, unsigned n, enode *const* args);
|
enode* mk(expr* f, unsigned generation, unsigned n, enode *const* args);
|
||||||
enode_vector const& enodes_of(func_decl* f);
|
enode_vector const& enodes_of(func_decl* f);
|
||||||
void push() { ++m_num_scopes; }
|
void push() { if (!m_to_merge.empty()) propagate(); ++m_num_scopes; }
|
||||||
void pop(unsigned num_scopes);
|
void pop(unsigned num_scopes);
|
||||||
|
|
||||||
/**
|
/**
|
||||||
|
|
Loading…
Reference in a new issue