mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
This commit is contained in:
parent
a48d3fdbb1
commit
0dd5a5e576
|
@ -149,6 +149,7 @@ public:
|
|||
bool is_store(expr* n) const { return is_app_of(n, m_fid, OP_STORE); }
|
||||
bool is_const(expr* n) const { return is_app_of(n, m_fid, OP_CONST_ARRAY); }
|
||||
bool is_ext(expr* n) const { return is_app_of(n, m_fid, OP_ARRAY_EXT); }
|
||||
bool is_ext(func_decl const* f) const { return is_decl_of(f, m_fid, OP_ARRAY_EXT); }
|
||||
bool is_map(expr* n) const { return is_app_of(n, m_fid, OP_ARRAY_MAP); }
|
||||
bool is_union(expr* n) const { return is_app_of(n, m_fid, OP_SET_UNION); }
|
||||
bool is_intersect(expr* n) const { return is_app_of(n, m_fid, OP_SET_INTERSECT); }
|
||||
|
|
|
@ -254,6 +254,7 @@ namespace array {
|
|||
void new_diseq_eh(euf::th_eq const& eq) override;
|
||||
bool unit_propagate() override;
|
||||
void init_model() override;
|
||||
bool include_func_interp(func_decl* f) const override { return a.is_ext(f); }
|
||||
void add_value(euf::enode* n, model& mdl, expr_ref_vector& values) override;
|
||||
bool add_dep(euf::enode* n, top_sort<euf::enode>& dep) override;
|
||||
sat::literal internalize(expr* e, bool sign, bool root, bool learned) override;
|
||||
|
|
|
@ -273,7 +273,6 @@ namespace euf {
|
|||
void solver::display_validation_failure(std::ostream& out, model& mdl, enode* n) {
|
||||
out << "Failed to validate " << n->bool_var() << " " << bpp(n) << " " << mdl(n->get_expr()) << "\n";
|
||||
s().display(out);
|
||||
return;
|
||||
euf::enode_vector nodes;
|
||||
nodes.push_back(n);
|
||||
for (unsigned i = 0; i < nodes.size(); ++i) {
|
||||
|
@ -327,9 +326,7 @@ namespace euf {
|
|||
CTRACE("euf", first, display_validation_failure(tout, mdl, n););
|
||||
(void)first;
|
||||
first = false;
|
||||
return;
|
||||
exit(1);
|
||||
first = false;
|
||||
}
|
||||
}
|
||||
|
||||
|
|
Loading…
Reference in a new issue