mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-22 22:03:39 +00:00
Code Activity

Merge pull request #1856 from waywardmonkeys/minor-fixes

Browse source 
Minor fixes
This commit is contained in:
Nikolaj Bjorner 2018-10-01 20:46:27 -07:00 • committed by GitHub
commit 2cf6ada38e
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
2 changed files with 4 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/smt/theory_lra.cpp
View file

@ -1569,7 +1569,6 @@ public:
VERIFY(a.is_idiv(n, p, q)); VERIFY(a.is_idiv(n, p, q));
theory_var v = mk_var(n); theory_var v = mk_var(n);
theory_var v1 = mk_var(p); theory_var v1 = mk_var(p);
theory_var v2 = mk_var(q);
rational r1 = get_value(v1); rational r1 = get_value(v1);
rational r2; rational r2;

8
src/smt/watch_list.cpp
View file

@ -36,10 +36,10 @@ namespace smt {
void watch_list::expand() { void watch_list::expand() {
if (m_data == nullptr) { if (m_data == nullptr) {
unsigned size = DEFAULT_WATCH_LIST_SIZE + HEADER_SIZE; unsigned size = DEFAULT_WATCH_LIST_SIZE + HEADER_SIZE;
unsigned * mem = reinterpret_cast<unsigned*>(alloc_svect(char, size)); unsigned * mem = reinterpret_cast<unsigned*>(alloc_svect(char, size));
#ifdef _AMD64_ #ifdef _AMD64_
++mem; // make sure data is aligned in 64 bit machines ++mem; // make sure data is aligned in 64 bit machines
#endif #endif
*mem = 0; *mem = 0;
++mem; ++mem;
@ -62,9 +62,9 @@ namespace smt {
unsigned * mem = reinterpret_cast<unsigned*>(alloc_svect(char, new_capacity + HEADER_SIZE)); unsigned * mem = reinterpret_cast<unsigned*>(alloc_svect(char, new_capacity + HEADER_SIZE));
unsigned curr_end_cls = end_cls_core(); unsigned curr_end_cls = end_cls_core();
#ifdef _AMD64_ #ifdef _AMD64_
++mem; // make sure data is aligned in 64 bit machines ++mem; // make sure data is aligned in 64 bit machines
#endif #endif
*mem = curr_end_cls; *mem = curr_end_cls;
++mem; ++mem;
SASSERT(bin_bytes <= new_capacity); SASSERT(bin_bytes <= new_capacity);
unsigned new_begin_bin = new_capacity - bin_bytes; unsigned new_begin_bin = new_capacity - bin_bytes;