mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

update slice/offset claim structures to allow for equal variable.

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-03-13 11:49:11 -07:00
parent 1e9381c2f6
commit 1f0a6c051a
1 changed files with 1 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/sat/smt/polysat_egraph.cpp
View file

@ -204,8 +204,7 @@ namespace polysat {
if (slice.child != null_var) {
auto c = var2enode(m_pddvar2var[slice.child]);
if (b != c)
m_bv_plugin->explain_slice(b, 0, c, consume_eq);
m_bv_plugin->explain_slice(b, 0, c, consume_eq);
}
}