Check not and minus better when type checking.

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

diff --git a/src/AST/ASTmisc.cpp b/src/AST/ASTmisc.cpp
index 4f01aa863077790e81ada5fd9d4ccfc755d176cd..e9a208be61e5b9951d578eb0cb4fb610c99b3db6 100644 (file)
--- a/src/AST/ASTmisc.cpp
+++ b/src/AST/ASTmisc.cpp
@@ -466,6 +466,8 @@ namespace BEEV
                        checkChildrenAreBV(v, n);
                        if (n.Degree() != 1)
                                FatalError("BVTypeCheck: should have exactly 1 args\n", n);
+                       if (n.GetValueWidth() != n[0].GetValueWidth())
+                         FatalError("BVTypeCheck: should have same value width\n", n);
                        break;
                case BVEXTRACT:
                        checkChildrenAreBV(v, n);