From 1067a5363f74c55f26f4146d993e6b923fdc478d Mon Sep 17 00:00:00 2001 From: Bruce Mitchener Date: Tue, 2 Oct 2018 08:34:57 +0700 Subject: [PATCH 1/2] theory_lra: Remove unused variable. --- src/smt/theory_lra.cpp | 1 - 1 file changed, 1 deletion(-) diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index d3475bdc1..171c4de0a 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -1569,7 +1569,6 @@ public: VERIFY(a.is_idiv(n, p, q)); theory_var v = mk_var(n); theory_var v1 = mk_var(p); - theory_var v2 = mk_var(q); rational r1 = get_value(v1); rational r2; From 6d2936e5fc20a26cac2ed37d39dd94d7d89f86f2 Mon Sep 17 00:00:00 2001 From: Bruce Mitchener Date: Tue, 2 Oct 2018 08:35:12 +0700 Subject: [PATCH 2/2] watch_list: Fix indentation. --- src/smt/watch_list.cpp | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/smt/watch_list.cpp b/src/smt/watch_list.cpp index 9835142f6..778e93021 100644 --- a/src/smt/watch_list.cpp +++ b/src/smt/watch_list.cpp @@ -36,10 +36,10 @@ namespace smt { void watch_list::expand() { if (m_data == nullptr) { - unsigned size = DEFAULT_WATCH_LIST_SIZE + HEADER_SIZE; + unsigned size = DEFAULT_WATCH_LIST_SIZE + HEADER_SIZE; unsigned * mem = reinterpret_cast(alloc_svect(char, size)); #ifdef _AMD64_ - ++mem; // make sure data is aligned in 64 bit machines + ++mem; // make sure data is aligned in 64 bit machines #endif *mem = 0; ++mem; @@ -62,9 +62,9 @@ namespace smt { unsigned * mem = reinterpret_cast(alloc_svect(char, new_capacity + HEADER_SIZE)); unsigned curr_end_cls = end_cls_core(); #ifdef _AMD64_ - ++mem; // make sure data is aligned in 64 bit machines + ++mem; // make sure data is aligned in 64 bit machines #endif - *mem = curr_end_cls; + *mem = curr_end_cls; ++mem; SASSERT(bin_bytes <= new_capacity); unsigned new_begin_bin = new_capacity - bin_bytes;