commit 981ae60780d0cc291b8fa6f13744c628da580c1a
author Trevor Hansen <trev_abroad@yahoo.com> Sun May 15 04:47:43 2022
committer Trevor Hansen <trev_abroad@yahoo.com> Sun May 15 04:47:43 2022
tree de3565d9d0504f87bd9f78e1892f627474df7b3e
parent b4347a89f6d64d3e604f673501f7073228af2a63

Extra simplification for bvmult.

lib/NodeFactory/SimplifyingNodeFactory.cpp

diff --git a/lib/NodeFactory/SimplifyingNodeFactory.cpp b/lib/NodeFactory/SimplifyingNodeFactory.cpp
index 9e3f133..936a229 100644
--- a/lib/NodeFactory/SimplifyingNodeFactory.cpp
+++ b/lib/NodeFactory/SimplifyingNodeFactory.cpp
@@ -1471,9 +1471,9 @@
                  children[0] == bm.CreateOneConst(width))
           result = children[1];
 
-        //else if (children[0].isConstant() &&
-          //       CONSTANTBV::BitVector_is_full(children[0].GetBVConst()))
-          //result = NodeFactory::CreateTerm(BVUMINUS, width, children[1]);
+        else if (children[0].isConstant() &&
+                 CONSTANTBV::BitVector_is_full(children[0].GetBVConst()))
+          result = NodeFactory::CreateTerm(BVUMINUS, width, children[1]);
 
         else if (width == 1 && children[0] == children[1])
           result = children[0];