mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 10:25:18 +00:00
Code Activity

let me guess, ASAN doesn't like 0-byte memcpy

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-08-03 23:19:59 -07:00
parent 90415a18d3
commit c7dc420b3b
1 changed files with 6 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/nlsat/nlsat_justification.h
View file

@ -46,8 +46,12 @@ namespace nlsat {
lazy_justification(unsigned nl, literal const * lits, unsigned nc, nlsat::clause * const* clss):
m_num_literals(nl),
m_num_clauses(nc) {
memcpy(m_data + 0, clss, sizeof(nlsat::clause const*)*nc);
memcpy(m_data + sizeof(nlsat::clause*)*nc, lits, sizeof(literal)*nl);
if (nc > 0) {
memcpy(m_data + 0, clss, sizeof(nlsat::clause*)*nc);
}
if (nl > 0) {
memcpy(m_data + sizeof(nlsat::clause*)*nc, lits, sizeof(literal)*nl);
}
}
unsigned num_lits() const { return m_num_literals; }
literal lit(unsigned i) const { SASSERT(i < num_lits()); return lits()[i]; }