From 278e0043858563bea5a8826a7a36d8a1fbd2f819 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 4 Jun 2020 01:28:26 -0700 Subject: [PATCH] fix #4428, and then there were none, almost Signed-off-by: Nikolaj Bjorner --- src/tactic/core/reduce_invertible_tactic.cpp | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/tactic/core/reduce_invertible_tactic.cpp b/src/tactic/core/reduce_invertible_tactic.cpp index 80b561d08..bfb5da408 100644 --- a/src/tactic/core/reduce_invertible_tactic.cpp +++ b/src/tactic/core/reduce_invertible_tactic.cpp @@ -204,15 +204,15 @@ private: return true; case OP_BMUL: + model = rational::one(); + return true; + case OP_BSDIV: case OP_BSDIV0: case OP_BSDIV_I: case OP_BUDIV: case OP_BUDIV0: case OP_BUDIV_I: - model = rational::one(); - return true; - default: return false; }