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; }