preconditions.py

And(Or(Not(-1*amount + _allowances[sender][msg.sender] <= -1),
       Not(amount == 0),
       Not(_balances[sender] >= amount),
       Not(amount >= 0),
       Not(recipient <= -1),
       Not(sender <= -1),
       Not(sender + -1*recipient <= -1),
       Not(0 <= _balances[recipient])),
    Or(_balances[sender] >= amount, Not(amount == 0)),
    Or(Not(amount == 0),
       0 <= _balances[recipient],
       sender == recipient),
    Or(Not(-1*amount + _allowances[sender][msg.sender] <= -1),
       Not(amount == 0),
       Not(_balances[sender] >= amount),
       Not(amount >= 0),
       Not(recipient >= 1),
       Not(sender >= 1),
       Not(-1*sender + recipient <= -1),
       Not(0 <= _balances[recipient])),
    Or(Not(0 == recipient), Not(amount == 0)),
    Or(Not(-1*amount + _allowances[sender][msg.sender] <= -1),
       Not(amount == 0),
       Not(_balances[sender] >= amount),
       Not(amount >= 0),
       Not(recipient <= -1),
       Not(sender <= -1),
       Not(-1*sender + recipient <= -1),
       Not(0 <= _balances[recipient])),
    Or(Not(0 == sender), Not(amount == 0)),
    Or(Not(-1*amount + _allowances[sender][msg.sender] <= -1),
       Not(amount == 0),
       Not(_balances[sender] >= amount),
       Not(amount >= 0),
       Not(recipient <= -1),
       Not(sender >= 1),
       Not(-1*sender + recipient <= -1),
       Not(0 <= _balances[recipient])),
    Or(Not(-1*amount + _allowances[sender][msg.sender] <= -1),
       Not(amount == 0),
       Not(_balances[sender] >= amount),
       Not(amount >= 0),
       Not(recipient >= 1),
       Not(sender >= 1),
       Not(sender + -1*recipient <= -1),
       Not(0 <= _balances[recipient])),
    Or(Not(-1*amount + _allowances[sender][msg.sender] <= -1),
       Not(amount == 0),
       Not(_balances[sender] >= amount),
       Not(amount >= 0),
       Not(recipient >= 1),
       Not(sender <= -1),
       Not(sender + -1*recipient <= -1),
       Not(0 <= _balances[recipient])),
    Or(Not(-1*amount + _allowances[sender][msg.sender] <= -1),
       Not(amount == 0),
       Not(-1*amount +
           _balances[sender] +
           -1*_balances[recipient] ==
           0),
       Not(_balances[sender] >= amount),
       Not(2*amount +
           -1*_balances[sender] +
           _balances[recipient] ==
           0),
       Not(amount >= 0),
       Not(recipient >= 1),
       Not(-1*recipient + sender == 0),
       Not(sender >= 1)),
    Or(Not(-1*amount + _allowances[sender][msg.sender] <= -1),
       Not(amount == 0),
       Not(-1*amount +
           _balances[sender] +
           -1*_balances[recipient] ==
           0),
       Not(_balances[sender] >= amount),
       Not(2*amount +
           -1*_balances[sender] +
           _balances[recipient] ==
           0),
       Not(amount >= 0),
       Not(-1*recipient + sender == 0),
       Not(recipient <= -1),
       Not(sender <= -1)))