From b68efe44afe486a00640e84ec9b78d0a73e30997 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 23 Feb 2020 12:28:15 -0800 Subject: [PATCH] fix fix Signed-off-by: Nikolaj Bjorner --- src/smt/theory_bv.cpp | 2 +- src/tactic/core/reduce_invertible_tactic.cpp | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/smt/theory_bv.cpp b/src/smt/theory_bv.cpp index 682b648fe..5335d463d 100644 --- a/src/smt/theory_bv.cpp +++ b/src/smt/theory_bv.cpp @@ -1801,7 +1801,7 @@ namespace smt { literal_vector const & bits2 = m_bits[v2]; theory_var v1 = v2; do { - literal_vector const & bits1 = m_bits[v1]; + literal_vector const & bits1 = m_bits[v1]; SASSERT(bits1.size() == bits2.size()); unsigned sz = bits1.size(); VERIFY(ctx.is_relevant(get_enode(v1))); diff --git a/src/tactic/core/reduce_invertible_tactic.cpp b/src/tactic/core/reduce_invertible_tactic.cpp index b664a9e26..697a67250 100644 --- a/src/tactic/core/reduce_invertible_tactic.cpp +++ b/src/tactic/core/reduce_invertible_tactic.cpp @@ -221,7 +221,7 @@ private: if (m_bv.is_numeral(arg, r) && r != mdl) return false; - if (i > 0 && (!is_app(arg) || to_app(arg)->get_num_args() > 0)) + if (i > 0 && !is_var(arg) && (!is_app(arg) || to_app(arg)->get_num_args() > 0)) return false; }