mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

Mark fixed_eq literals as relevant (#7533)

Browse source
This commit is contained in:
Can Cebeci 2025-01-27 20:10:46 +01:00 committed by GitHub
parent 63f9fdaf3e
commit 2d8f024680
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 2 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/smt/theory_bv.cpp
View file

@ -441,6 +441,8 @@ namespace smt {
app* o1 = get_enode(v1)->get_expr(); app* o1 = get_enode(v1)->get_expr();
app* o2 = get_enode(v2)->get_expr(); app* o2 = get_enode(v2)->get_expr();
literal oeq = mk_eq(o1, o2, true); literal oeq = mk_eq(o1, o2, true);
ctx.mark_as_relevant(oeq);
unsigned sz = get_bv_size(v1); unsigned sz = get_bv_size(v1);
TRACE("bv", TRACE("bv",
tout << mk_pp(o1, m) << " = " << mk_pp(o2, m) << " " tout << mk_pp(o1, m) << " = " << mk_pp(o2, m) << " "