mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-16 05:48:44 +00:00
Code Activity

fix #6157

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-07-13 14:37:04 -07:00
parent a3eb9da191
commit 1378e713ba
1 changed files with 3 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/smt/theory_bv.cpp
View file

@ -667,8 +667,9 @@ namespace smt {
mk_enode(n); mk_enode(n);
theory_var v = ctx.get_enode(n)->get_th_var(get_id()); theory_var v = ctx.get_enode(n)->get_th_var(get_id());
mk_bits(v); mk_bits(v);
mk_var(ctx.get_enode(n->get_arg(0))); enode* k = ctx.get_enode(n->get_arg(0));
if (!is_attached_to_var(k))
mk_var(k);
if (!ctx.relevancy()) if (!ctx.relevancy())
assert_int2bv_axiom(n); assert_int2bv_axiom(n);