Minor cleanup.

* Reenable parts of bvsimple test
* Fix typo in #endif comment

diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index b4d20b514c9f6b292a7dcdb91977904be163a419..15c49efd80cb1cf15068dbd9f6954b2b1ca22c45 100644 (file)
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -1476,4 +1476,4 @@ NodeClass NodeManager::mkConstInternal(const T& val) {
 
 }/* CVC4 namespace */
 
-#endif /* __CVC4__EXPR_MANAGER_H */
+#endif /* __CVC4__NODE_MANAGER_H */

diff --git a/test/regress/regress0/bv/bvsimple.cvc b/test/regress/regress0/bv/bvsimple.cvc
index be57075548e0c64bab0e7e786ba182c7c1f7ba09..dcacd643a3ed8a845958d5cf76e0a6c23678b6e0 100644 (file)
--- a/test/regress/regress0/bv/bvsimple.cvc
+++ b/test/regress/regress0/bv/bvsimple.cvc
@@ -22,22 +22,19 @@ QUERY
 ( 0bin0011 << 3 = 0bin0011000 ) AND
 ( 0bin1000 >> 3 = 0bin0001 ) AND
 
-% these not working yet..
-%
-%( BVZEROEXTEND(0bin100, 2) = 0bin00100 ) AND
-%( SX(0bin100, 5) = 0bin11100 ) AND
-%
-%( BVZEROEXTEND(0bin100, 0) = 0bin100 ) AND
-%( SX(0bin100, 3) = 0bin100 ) AND
-%
-%( (BVPLUS(9, x@0bin0000, (0bin000@(~y)@0bin11)))[8:4] = BVPLUS(5, x, ~(y[3:2])) ) AND
-%
-%( x4 = 0hex5 AND y4 = 0bin0101 ) =>
-%( ( BVMULT(8,x4,y4)=BVMULT(8,y4,x4) ) AND
-%  ( NOT(BVLT(x4,y4)) ) AND
-%  ( BVLE(BVSUB(8,x4,y4), BVPLUS(8, x4, BVUMINUS(x4))) ) AND
-%  ( x4 = BVSUB(4, BVUMINUS(x4), BVPLUS(4, x4,0hex1)) ) ) AND
+( BVZEROEXTEND(0bin100, 2) = 0bin00100 ) AND
+( SX(0bin100, 5) = 0bin11100 ) AND
 
+( BVZEROEXTEND(0bin100, 0) = 0bin100 ) AND
+( SX(0bin100, 3) = 0bin100 ) AND
+
+( (BVPLUS(9, x@0bin0000, (0bin000@(~y)@0bin11)))[8:4] = BVPLUS(5, x, ~(y[3:2])) ) AND
+
+( x4 = 0hex5 AND y4 = 0bin0101 ) =>
+( ( BVMULT(8,x4,y4)=BVMULT(8,y4,x4) ) AND
+  ( NOT(BVLT(x4,y4)) ) AND
+  ( BVLE(BVSUB(8,x4,y4), BVPLUS(8, x4, BVUMINUS(x4))) ) AND
+  ( x4 = BVSUB(4, BVUMINUS(x4), BVPLUS(4, x4,0hex1)) ) ) AND
 
 ( 0bin01100000[5:3]=(0bin1111001@bv[0:0])[4:2] ) AND
 ( 0bin1@(IF a THEN 0bin0 ELSE 0bin1 ENDIF) = (IF a THEN 0bin110 ELSE 0bin011 ENDIF)[1:0] ) AND