memory: move byte size > bits_size_t check to is_dereferenceable
MODIFY
ir/instr.cpp
ir/instr.cpp
@@ -2131,11 +2131,6 @@ StateValue Memset::toSMT(State &s) const {
auto &[vbytes, np_bytes] = s[*bytes];
s.addUB((vbytes != 0).implies(np_ptr));
s.addUB(np_bytes);
-
- if (vbytes.bits() > bits_size_t)
- s.addUB(
- vbytes.ule(expr::IntUMax(bits_size_t).zext(vbytes.bits() - bits_size_t)));
-
s.getMemory().memset(vptr, s[*val].zextOrTrunc(8), vbytes, align);
return {};
}

MODIFY
ir/memory.cpp
ir/memory.cpp
@@ -598,6 +598,10 @@ void Pointer::is_dereferenceable(const expr &bytes0, unsigned align,
m.state->addUB(bytes == 0 || *UB());
+ // cannot store more bytes than address space
+ if (bytes0.bits() > bits_size_t)
+ m.state->addUB(bytes0.extract(bytes0.bits() - 1, bits_size_t) == 0);
+
// address must be always aligned regardless of access size
m.state->addUB(*is_aligned());

MODIFY
util/sort.h
util/sort.h
// Copyright (c) 2018-present The Alive2 Authors.
// Distributed under the MIT license that can be found in the LICENSE file.
-#include <string>
#include <unordered_set>
#include <vector>

memory: move byte size > bits_size_t check to is_dereferenceable