add filter to detect circumventing the default semantics of bit-vector division with the use of the sat-based bit-vector solver. Provides a way to fix issue #190

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

src/ast/rewriter/bv_rewriter.h

@@ -168,6 +168,8 @@ public:
     }
 
     br_status mk_eq_core(expr * lhs, expr * rhs, expr_ref & result);
+
+    bool hi_div0() const { return m_hi_div0; }
 };
 
 #endif