I call satisfy_one with assumptions for expression which is not in CNF form. Then it calls _backtrackhere, receives None because restricted expression is unsatisfiable and crashes at next line.
Something like this would fix the problem:
soln = _backtrack(self.restrict(aupnt))
return None if soln is None else soln.update(aupnt)
I call
satisfy_onewith assumptions for expression which is not in CNF form. Then it calls_backtrackhere, receivesNonebecause restricted expression is unsatisfiable and crashes at next line.Something like this would fix the problem: