From edb3c9c0dc95349a3136f8b83271e1a704c5f799 Mon Sep 17 00:00:00 2001
From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Sun, 10 Dec 2017 17:01:25 -0800
Subject: minor fix

---
 src/theory/bv/theory_bv_rewrite_rules_simplification.h | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

diff --git a/src/theory/bv/theory_bv_rewrite_rules_simplification.h b/src/theory/bv/theory_bv_rewrite_rules_simplification.h
index 91a70c812..ee9953b23 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_simplification.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_simplification.h
@@ -19,7 +19,6 @@
 
 #pragma once
 
-#include "options/bv_options.h"
 #include "theory/bv/theory_bv_rewrite_rules.h"
 #include "theory/bv/theory_bv_utils.h"
 #include "theory/rewriter.h"
@@ -953,8 +952,7 @@ inline Node RewriteRule<UdivOne>::apply(TNode node) {
 
 template <>
 inline bool RewriteRule<UdivConst>::applies(TNode node) {
-  return (!options::bitvectorDivByZeroConst() &&
-          node.getKind() == kind::BITVECTOR_UDIV_TOTAL &&
+  return (node.getKind() == kind::BITVECTOR_UDIV_TOTAL &&
           node[1].getKind() == kind::CONST_BITVECTOR &&
           node[1] != utils::mkConst(utils::getSize(node[1]), 0));
 }
-- 
cgit v1.2.3