mirror of
https://github.com/Z3Prover/z3
synced 2025-07-22 20:32:05 +00:00
validate sls-arith lemmas
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
c6f5e3232c
commit
6f37da5a07
1 changed files with 2 additions and 0 deletions
|
@ -1273,6 +1273,8 @@ namespace arith {
|
||||||
c.neg();
|
c.neg();
|
||||||
DEBUG_CODE(for (literal c : m_core) { SASSERT(s().value(c) != l_true); });
|
DEBUG_CODE(for (literal c : m_core) { SASSERT(s().value(c) != l_true); });
|
||||||
|
|
||||||
|
for (literal c : m_core) { VERIFY(s().value(c) != l_true); }
|
||||||
|
|
||||||
add_redundant(m_core, explain(ty));
|
add_redundant(m_core, explain(ty));
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
Loading…
Add table
Add a link
Reference in a new issue