Bram-Hub/Willow

Instantiating a universal whose variable does not appear in the formula results in an error

Opened this issue · 1 comments

The following decomposition in a truth tree results in an error:

forall x forall y P(y)
forall y P(y)

This is because the code does not know to what constant the user is trying to assign x. If the variable does not appear in the formula, the assignment code should assume an arbitrary value (which will necessarily be valid since the constant will not appear in the resulting formula).

This fix does not introduce that new constant to the universe, but prevents crashing when running into this scenario.