diff --git a/src/methods/nnf/NodeManager.hpp b/src/methods/nnf/NodeManager.hpp index fdc90d27..2f79d2cb 100644 --- a/src/methods/nnf/NodeManager.hpp +++ b/src/methods/nnf/NodeManager.hpp @@ -252,8 +252,10 @@ class NodeManager { @param[in] nbVar, the number of variables in the problem. */ static NodeManager *makeNodeManager(unsigned nbVar) { - if (nbVar < (1 << 8)) return new NodeManagerTyped(); - if (nbVar < (1 << 16)) return new NodeManagerTyped(); + // One bit is reserved for the sign of the variable. + // Hence, with 8 bits we can store variables from -(2⁷-1) up to 2⁷-1. Same holds for 16 and 32 bits. + if (nbVar < (1 << 7)) return new NodeManagerTyped(); + if (nbVar < (1 << 15)) return new NodeManagerTyped(); return new NodeManagerTyped(); } // makeNodeManager