module main {
  var a, b : integer;
  init {
    a = 0;
    b = 1;
  }
  next {
    a', b' = b, a+b;
  }

  // Part 2: System specification
  invariant a_le_b: a <= b;

  // Part 3: Proof script
  control {
    // original uclid was like SRI's sat tool
    //bmc(3); // do bounded model checking for 3 steps
    //induction;
    vobj = induction(1);  // do induction for one step

    check; // call smt solver
    print_results;

    vobj.print_cex(a, b);  // print counterexample on failure
  }
}

// uclid name.ucl
// uclid name.ucl (failed ∵ invariant not powerful enough)

// uclid name.ucl -m Sys // check Sys module instead of main module