mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 05:18:44 +00:00
Code Activity

fix #3678

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-04-03 13:28:28 -07:00
parent a119953676
commit b642686dca
1 changed files with 5 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/smt/theory_diff_logic_def.h
View file

@ -841,8 +841,8 @@ void theory_diff_logic<Ext>::reset_eh() {
dealloc(m_atoms[i]);
}
m_graph .reset();
m_izero = null_theory_var;
m_rzero = null_theory_var;
m_izero = null_theory_var;
m_rzero = null_theory_var;
m_atoms .reset();
m_asserted_atoms .reset();
m_stats .reset();
@ -1109,6 +1109,7 @@ unsigned theory_diff_logic<Ext>::simplex2edge(unsigned e) {
template<typename Ext>
void theory_diff_logic<Ext>::update_simplex(Simplex& S) {
m_graph.set_to_zero(get_zero(true), get_zero(false));
unsynch_mpq_inf_manager inf_mgr;
unsynch_mpq_manager& mgr = inf_mgr.get_mpq_manager();
unsigned num_nodes = m_graph.get_num_nodes();
@ -1193,7 +1194,8 @@ typename theory_diff_logic<Ext>::inf_eps theory_diff_logic<Ext>::value(theory_va
template<typename Ext>
typename theory_diff_logic<Ext>::inf_eps
theory_diff_logic<Ext>::maximize(theory_var v, expr_ref& blocker, bool& has_shared) {
SASSERT(is_consistent());
has_shared = false;
Simplex& S = m_S;
ast_manager& m = get_manager();