mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-05 21:53:23 +00:00
Code Activity

fix a few build regressions

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-06-14 08:34:52 -07:00 • committed by Arie Gurfinkel
parent e355123e37
commit bc8ddedc54
4 changed files with 5 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/api/api_solver.cpp
View file

@ -536,7 +536,6 @@ extern "C" {
init_solver(c, s); init_solver(c, s);
expr_ref_vector _assumptions(m), _consequences(m), _variables(m); expr_ref_vector _assumptions(m), _consequences(m), _variables(m);
ast_ref_vector const& __assumptions = to_ast_vector_ref(assumptions); ast_ref_vector const& __assumptions = to_ast_vector_ref(assumptions);
unsigned sz = __assumptions.size();
for (ast* e : __assumptions) { for (ast* e : __assumptions) {
if (!is_expr(e)) { if (!is_expr(e)) {
_assumptions.finalize(); _consequences.finalize(); _variables.finalize(); _assumptions.finalize(); _consequences.finalize(); _variables.finalize();
@ -546,7 +545,6 @@ extern "C" {
_assumptions.push_back(to_expr(e)); _assumptions.push_back(to_expr(e));
} }
ast_ref_vector const& __variables = to_ast_vector_ref(variables); ast_ref_vector const& __variables = to_ast_vector_ref(variables);
sz = __variables.size();
for (ast* a : __variables) { for (ast* a : __variables) {
if (!is_expr(a)) { if (!is_expr(a)) {
_assumptions.finalize(); _consequences.finalize(); _variables.finalize(); _assumptions.finalize(); _consequences.finalize(); _variables.finalize();

1
src/ast/arith_decl_plugin.cpp
View file

@ -401,6 +401,7 @@ inline decl_kind arith_decl_plugin::fix_kind(decl_kind k, unsigned arity) {
app * arith_decl_plugin::mk_numeral(rational const & val, bool is_int) { app * arith_decl_plugin::mk_numeral(rational const & val, bool is_int) {
if (is_int && !val.is_int()) { if (is_int && !val.is_int()) {
SASSERT(false);
m_manager->raise_exception("invalid rational value passed as an integer"); m_manager->raise_exception("invalid rational value passed as an integer");
} }
if (val.is_unsigned()) { if (val.is_unsigned()) {

4
src/qe/qe_solve_plugin.cpp
View file

@ -80,8 +80,8 @@ namespace qe {
bool sign = todo.back().first; bool sign = todo.back().first;
todo.pop_back(); todo.pop_back();
if (a.is_add(e)) { if (a.is_add(e)) {
for (expr* e : *to_app(e)) { for (expr* arg : *to_app(e)) {
todo.push_back(std::make_pair(sign, e)); todo.push_back(std::make_pair(sign, arg));
} }
} }
else if (a.is_sub(e)) { else if (a.is_sub(e)) {

4
src/smt/smt_setup.cpp
View file

@ -730,8 +730,8 @@ namespace smt {
} }
void setup::setup_i_arith() { void setup::setup_i_arith() {
m_context.register_plugin(alloc(smt::theory_lra, m_manager, m_params)); // m_context.register_plugin(alloc(smt::theory_lra, m_manager, m_params));
// m_context.register_plugin(alloc(smt::theory_i_arith, m_manager, m_params)); m_context.register_plugin(alloc(smt::theory_i_arith, m_manager, m_params));
} }
void setup::setup_r_arith() { void setup::setup_r_arith() {