// Please select one of the following scripts.
//
script testSMT(){
    smt solver='Z3';
}
script toRemove(){
  impRight;
  useContract type='dependency' on=`p`;

}

script autoScript(){
    __STRICT_MODE := true;
    auto;
}

script interactive(){
  impRight;
  impRight;
  impLeft;

}

script interactive_with_match(){
impRight;
impRight;
impLeft;
cases{
    case match `==> !(?Z), ?Z`:
      notRight;

    default:
      notLeft;

    }

}