text: function add(x_0, x_1)
  {
  	return x_0 + x_1;
  }
  
  function mult(x_0, x_1)
  {
  	return x_0 * x_1;
  }
  
  function concat(x_0, x_1)
  {
  	return x_0 + x_1;
  }
  
  function len(x_0)
  {
  	return x_0.length;
  }
  
  function toStr(x_0)
  {
  	return x_0 + "";
  }
  
  function beforeAfter(x_0)
  {
  	return 'B' + x_0 + 'A';
  }
  
  //@pbe (constraint (= (f998f 0) 0))
  //@pbe (constraint (= (f998f 7) 56))