fix #4428, and then there were none, almost

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

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