mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-09 20:50:50 +00:00
Code Activity

Merge branch 'master' into polysat

Browse source
This commit is contained in:
Jakob Rath 2022-08-01 15:03:03 +02:00
commit 0f51f3ed17
10 changed files with 26 additions and 41 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/smt/theory_special_relations.cpp
View file

@ -135,7 +135,7 @@ namespace smt {
bool theory_special_relations::internalize_atom(app * atm, bool gate_ctx) {
SASSERT(m_util.is_special_relation(atm));
relation* r = 0;
relation* r = nullptr;
ast_manager& m = get_manager();
if (!m_relations.find(atm->get_decl(), r)) {
r = alloc(relation, m_util.get_property(atm), atm->get_decl(), m);
@ -470,7 +470,7 @@ namespace smt {
ctx.mk_justification(
ext_theory_conflict_justification(
get_id(), ctx.get_region(),
lits.size(), lits.data(), 0, 0, params.size(), params.data())));
lits.size(), lits.data(), 0, nullptr, params.size(), params.data())));
}
lbool theory_special_relations::final_check(relation& r) {