// Purpose: we should throw an error when we ask UCLID to print a counterexample from a verification result variable that is not defined.
// Description: A uclid module with a control block that uses the command x.print_cex(), when x is not defined
// Expectation: UCLID should throw an error
// Validation: revert dbff1a0a082b97864b1a77d40e6e052c2be9d84d

module main {
  init { }
  next { }

  control {
    induction;
    check;
    print_results;
   x.print_cex(); // this will parse fine but get ignored
  }
