---

And.java

package gov.nasa.arc.ase.jpf.expr;

//#ifdef BUCHI
class And implements SubExpr {
  private int length;
  private SubExpr[] terms;
  
  And(int l) {
    length = l;
    terms = new SubExpr[l];
  }  
  public void backtrack() {
    throw new RuntimeException("Expression is not executable");
  }  
  public boolean evaluate() {
    boolean result = true;

    for(int i = 0; result && i < length; i++)
      result &= terms[i].evaluate();

    return result;
  }  
  public void execute() {
    throw new RuntimeException("Expression is not executable");
  }  
  void set(int index, SubExpr t) {
    terms[index] = t;
  }  
  public String toString() {
    StringBuffer sb = new StringBuffer();

    for(int i = 0; i < length; i++) {
      if(i != 0) sb.append(" & ");
      sb.append(terms[i]);
    }

    return sb.toString();
  }  
}

---