actually remove _id from Term, fix goof with TERM_DIST_VAR_UNKNOWN

vprover · Dec 14, 2023 · 3d5dcef · 3d5dcef
1 parent 31939a4
commit 3d5dcef
Showing 1 changed file with 2 additions and 3 deletions.
diff --git a/Kernel/Term.hpp b/Kernel/Term.hpp
@@ -40,7 +40,8 @@
 
 // the number of bits used for "TermList::_info::distinctVars"
 #define TERM_DIST_VAR_BITS 21
-#define TERM_DIST_VAR_UNKNOWN ((2 ^ TERM_DIST_VAR_BITS) - 1)
+// maximum number that fits in a 21-bit integer - update if TERM_DIST_VAR_BITS changes
+#define TERM_DIST_VAR_UNKNOWN 0x1FFFFF
 
 namespace Kernel {
 
@@ -789,8 +790,6 @@ class Term
     _args[0]._info.order = val;
   }
 
-  /** For shared terms, this is a unique id used for deterministic comparison */
-  unsigned _id;
   /** The number of this symbol in a signature */
   unsigned _functor;
   /** Arity of the symbol */