Skip to content

Commit 081d296

Browse files
committed
avoid duplicating memory axioms for src & tgt
1 parent 4cbbd97 commit 081d296

File tree

1 file changed

+2
-4
lines changed

1 file changed

+2
-4
lines changed

ir/memory.cpp

Lines changed: 2 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1338,8 +1338,7 @@ static expr mk_liveness_array() {
13381338
}
13391339

13401340
void Memory::mkNonPoisonAxioms(bool local) const {
1341-
expr offset
1342-
= expr::mkFreshVar("#off", expr::mkUInt(0, Pointer::bitsShortOffset()));
1341+
expr offset = expr::mkVar("#axoff", Pointer::bitsShortOffset());
13431342

13441343
unsigned bid = 0;
13451344
for (auto &block : local ? local_block_val : non_local_block_val) {
@@ -1386,8 +1385,7 @@ void Memory::mkNonlocalValAxioms(bool skip_consts) const {
13861385
if (!does_ptr_mem_access && !(num_sub_byte_bits && isAsmMode()))
13871386
return;
13881387

1389-
expr offset
1390-
= expr::mkFreshVar("#off", expr::mkUInt(0, Pointer::bitsShortOffset()));
1388+
expr offset = expr::mkVar("#axoff", Pointer::bitsShortOffset());
13911389

13921390
for (unsigned i = 0, e = numNonlocals(); i != e; ++i) {
13931391
if (always_noread(i, true))

0 commit comments

Comments
 (0)