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

fix #2763

Browse source
This commit is contained in:
Nikolaj Bjorner 2019-12-01 17:10:21 -08:00
parent ad309e53a1
commit 86c35bc7c1
2 changed files with 11 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
src/smt/theory_lra.cpp
View file

@ -974,6 +974,12 @@ public:
m_arith_eq_adapter.new_diseq_eh(v1, v2);
}
void apply_sort_cnstr(enode* n, sort*) {
if (!th.is_attached_to_var(n)) {
mk_var(n->get_owner(), false);
}
}
void push_scope_eh() {
TRACE("arith", tout << "push\n";);
m_scopes.push_back(scope());
@ -1393,7 +1399,6 @@ public:
if (v == null_theory_var ||
v >= static_cast<theory_var>(m_theory_var2var_index.size())) {
TRACE("arith", tout << "Variable v" << v << " not internalized\n";);
return rational::zero();
}
@ -1402,7 +1407,6 @@ public:
return m_variable_values[vi];
if (!m_solver->is_term(vi)) {
TRACE("arith", tout << "not a term v" << v << "\n";);
return rational::zero();
}
@ -3591,6 +3595,9 @@ bool theory_lra::use_diseqs() const {
void theory_lra::new_diseq_eh(theory_var v1, theory_var v2) {
m_imp->new_diseq_eh(v1, v2);
}
void theory_lra::apply_sort_cnstr(enode* n, sort* s) {
m_imp->apply_sort_cnstr(n, s);
}
void theory_lra::push_scope_eh() {
theory::push_scope_eh();
m_imp->push_scope_eh();

2
src/smt/theory_lra.h
View file

@ -75,6 +75,8 @@ namespace smt {
void reset_eh() override;
void apply_sort_cnstr(enode * n, sort * s) override;
void init_model(model_generator & m) override;
model_value_proc * mk_value(enode * n, model_generator & mg) override;