Closed NickF0211 closed 1 year ago
Monosat could run into segmentation faults when parsing BV equality predicate atoms with negative external variables.
For example: bv const != -20 x y
MonoSAT checks wether the external variable (-20) already exists or not by calling:
inline bool inVarMap(Var externalVar){ if(externalVar == var_Undef){ return false; } return externalVar < var_map.size() && var_map[externalVar] != var_Undef; }
where var_map is accessed with a negative index.
To fix this issue, if the external variable x is negative , we can process -x instead. Doing so would require flipping the sign for equality (inequality).
Thank you, Nick
Monosat could run into segmentation faults when parsing BV equality predicate atoms with negative external variables.
For example: bv const != -20 x y
MonoSAT checks wether the external variable (-20) already exists or not by calling:
inline bool inVarMap(Var externalVar){ if(externalVar == var_Undef){ return false; } return externalVar < var_map.size() && var_map[externalVar] != var_Undef; }
where var_map is accessed with a negative index.
To fix this issue, if the external variable x is negative , we can process -x instead. Doing so would require flipping the sign for equality (inequality).
Thank you, Nick