mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-29 03:45:51 +00:00
Code Activity

fix #2912

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-02-01 17:32:19 -08:00
parent 321329d77c
commit be95ea121b
3 changed files with 4 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/ast/ast.cpp
View file

@ -2284,7 +2284,6 @@ void ast_manager::check_args(func_decl* f, unsigned n, expr* const* es) {
<< " for function " << mk_pp(f,*this)
<< " supplied sort is "
<< mk_pp(actual_sort, *this);
SASSERT(false);
throw ast_exception(buffer.str());
}
}

2
src/smt/smt_internalizer.cpp
View file

@ -444,7 +444,7 @@ namespace smt {
if (!gate_ctx) {
mk_enode(n, true, true, false);
set_enode_flag(v, true);
SASSERT(get_assignment(v) == l_undef);
SASSERT(get_assignment(v) == l_undef || get_assignment(l_def) != l_undef);
}
}

5
src/smt/theory_arith_nl.h
View file

@ -1541,10 +1541,10 @@ expr * theory_arith<Ext>::cross_nested(sbuffer<coeff_expr> & p, expr * var) {
rational a, b;
unsigned n = UINT_MAX;
unsigned nm = UINT_MAX;
if (in_monovariate_monomials(p, var, i1, a, n, i2, b, nm)) {
if (in_monovariate_monomials(p, var, i1, a, n, i2, b, nm)) {
CTRACE("in_monovariate_monomials", n == nm,
for (unsigned i = 0; i < p.size(); i++) {
if (i > 0) tout << " + "; tout << p[i].first << "*" << mk_pp(p[i].second, get_manager());
if (i > 0) tout << " + "; tout << p[i].first << "*" << mk_pp(p[i].second, get_manager());
}
tout << "\n";
tout << "var: " << mk_pp(var, get_manager()) << "\n";
@ -1554,6 +1554,7 @@ expr * theory_arith<Ext>::cross_nested(sbuffer<coeff_expr> & p, expr * var) {
tout << "i2: " << i2 << "\n";
tout << "b: " << b << "\n";
tout << "nm: " << nm << "\n";);
if (n == nm) return horner(p, var);
SASSERT(n != nm);
expr * new_expr = nullptr;
if (nm < n) {