ERC20Basic.sol

contract ERC20Basic {

  string public constant name = "ERC20Basic";
  string public constant symbol = "BSC";
  uint8 public constant decimals = 18;


  event Approval(address indexed tokenOwner, address indexed spender, uint tokens);
  event Transfer(address indexed from, address indexed to, uint tokens);


  mapping(address => uint256) balances;

  mapping(address => mapping(address => uint256)) allowed;

  uint256 totalSupply_;

  using SafeMath for uint256;

  constructor(uint256 total) public {
    totalSupply_ = total;
    balances[msg.sender] = totalSupply_;
  }

  function totalSupply() public view returns(uint256) {
    return totalSupply_;
  }

  function balanceOf(address tokenOwner) public view returns(uint) {
    return balances[tokenOwner];
  }

  function transfer(address receiver, uint numTokens) public returns(bool) {
    require(numTokens <= balances[msg.sender]);
    balances[msg.sender] = balances[msg.sender].sub(numTokens);
    balances[receiver] = balances[receiver].add(numTokens);
    emit Transfer(msg.sender, receiver, numTokens);
    return true;
  }

  function approve(address delegate, uint numTokens) public returns(bool) {
    allowed[msg.sender][delegate] = numTokens;
    Approval(msg.sender, delegate, numTokens);
    return true;
  }

  function allowance(address owner, address delegate) public view returns(uint) {
    return allowed[owner][delegate];
  }

  function transferFrom(address owner, address buyer, uint numTokens) public returns(bool) {
    require(numTokens <= balances[owner]);
    require(numTokens <= allowed[owner][msg.sender]);

    balances[owner] = balances[owner].sub(numTokens);
    allowed[owner][msg.sender] = allowed[owner][msg.sender].sub(numTokens);
    balances[buyer] = balances[buyer].add(numTokens);
    Transfer(owner, buyer, numTokens);
    return true;
  }
}

ERC20BasicSpec.py

uint x = balances[msg.sender]
uint y = balances[*]
uint z = balances[**]
uint m = allowed[**][msg.sender]
uint n = allowed[msg.sender][*]

init(uint k = total):
  (x = k) if k > 0
transfer(uint k = numTokens):
  (x, y) -> (x - k, y + k) if k > 0
approve(uint k = numTokens):
  (n) -> (n + k) if k > 0
transferFrom(uint k = numTokens):
  (m, y, z) -> (m - k, y + k, z - k) if k > 0

Instrumented.sol

contract ERC20Basic {

  string public constant name = "ERC20Basic";
  string public constant symbol = "BSC";
  uint8 public constant decimals = 18;


  event Approval(address indexed tokenOwner, address indexed spender, uint tokens);
  event Transfer(address indexed from, address indexed to, uint tokens);


  mapping(address => uint256) balances;

  mapping(address => mapping(address => uint256)) allowed;

  uint256 totalSupply_;

  using SafeMath for uint256;

  constructor(uint256 total) public {
    assert(total > 0); // INJECTED
    totalSupply_ = total;
    balances[msg.sender] = totalSupply_;
    assert(balances[msg.sender] == total); // INJECTED
  }

  function totalSupply() public view returns(uint256) {
    return totalSupply_;
  }

  function balanceOf(address tokenOwner) public view returns(uint) {
    return balances[tokenOwner];
  }

  function transfer(address receiver, uint numTokens) public returns(bool) {
    uint (x, y) = (balances[msg.sender], balances[receiver]); // INJECTED
    assert(numTokens <= balances[msg.sender]); // INJECTED
    assert(balances[msg.sender] >= numTokens); // INJECTED
    assert(balances[receiver] + numTokens > numTokens); // INJECTED 
    require(numTokens <= balances[msg.sender]);
    balances[msg.sender] = balances[msg.sender].sub(numTokens);
    balances[receiver] = balances[receiver].add(numTokens);
    emit Transfer(msg.sender, receiver, numTokens);
    assert(balances[msg.sender] + numTokens == x); // INJECTED
    assert(y + numTokens == balances[receiver]); // INJECTED
    return true;
  }

  function approve(address delegate, uint numTokens) public returns(bool) {
    assert(numTokens > 0); // INJECTED
    allowed[msg.sender][delegate] = numTokens;
    Approval(msg.sender, delegate, numTokens);
    assert(allowed[msg.sender][delegate] == numTokens) // INJECTED
    return true;
  }

  function allowance(address owner, address delegate) public view returns(uint) {
    return allowed[owner][delegate];
  }
   
  function transferFrom(address owner, address buyer, uint numTokens) public returns(bool) {
    uint (m, y, z) = (allowed[owner][msg.sender], balances[buyer], balances[owner]); // INJECTED
    assert(numTokens > 0); // INJECTED
    assert(allowed[owner][msg.sender] >= numTokens); // INJECTED
    assert(balances[buyer] + numTokens > numTokens); // INJECTED
    assert(balances[owner] >= numTokens); // INJECTED
    
    require(numTokens <= balances[owner]);
    require(numTokens <= allowed[owner][msg.sender]);

    balances[owner] = balances[owner].sub(numTokens);
    allowed[owner][msg.sender] = allowed[owner][msg.sender].sub(numTokens);
    balances[buyer] = balances[buyer].add(numTokens);
    Transfer(owner, buyer, numTokens);
    
    assert(allowed[owner][msg.sender] + numTokens == m); // INJECTED
    assert(y + numTokens == balances[buyer]); // INJECTED
    assert(balances[owner] + numTokens = z); // INJECTED
    
    return true;
  }
}