Segfault when attempting 0/1 equiv 0/1

cjdrake / boolexpr

Boolean Expressions

Apache License 2.0

20 stars 6 forks source link

Segfault when attempting 0/1 equiv 0/1 #15

Closed cjdrake closed 8 years ago

cjdrake commented 8 years ago

>>> from boolexpr import ZERO
>>> ZERO.equiv(ZERO)
Segmentation fault (core dumped)

>>> from boolexpr import ONE
>>> ONE.equiv(ONE)
Segmentation fault (core dumped)

cjdrake commented 8 years ago

Problem is in Operator::sat(). Since Tseytin transform doesn't simplify, you end up with 0/1 at the leaf nodes, and the code assumes literals.