Improve type checking for BVZX & BVSX.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@103 e59a4935-1847-0410-ae03-e826735625c1

diff --git a/AST/AST.cpp b/AST/AST.cpp
index 7f44c3516caf2188a0cc1dd17ca8e863156d0066..509880e892f4e665daf99353701401bd2f0f81f1 100644 (file)
--- a/AST/AST.cpp
+++ b/AST/AST.cpp
@@ -1365,6 +1365,8 @@ bool BeevMgr::BVTypeCheck(const ASTNode& n)
                                {
                                        FatalError("BVTypeCheck: BVSX(t,bvsx_len) : length of 't' must be <= bvsx_len\n", n);
                                }
+                               if ((v.size() != 2))
+                                               FatalError("BVTypeCheck:BVSX must have two arguments. The second is the new width\n", n);
                                break;
 
                        case BVZX:
@@ -1374,6 +1376,9 @@ bool BeevMgr::BVTypeCheck(const ASTNode& n)
                                {
                                        FatalError("BVTypeCheck: BVZX(t,bvzx_len) : length of 't' must be <= bvzx_len\n", n);
                                }
+                               if ((v.size() != 2))
+                                               FatalError("BVTypeCheck:BVZX must have two arguments. The second is the new width\n", n);
+
                                break;
 
                        default: