From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Sat, 8 Mar 2014 06:38:25 +0000 (-0500)
Subject: Minor cleanup.
X-Git-Tag: cvc5-1.0.0~7027
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=21c71dd206b2b131ee12c811bd7b0997de07adfa;p=cvc5.git

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 b4d20b514..15c49efd8 100644
--- 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 be5707554..dcacd643a 100644
--- 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