node root(In : int; C : bool) returns (Out, Out1 : int)
var last_Out, last_Out1: int;
    isp, isn: bool;
let
  last_Out = 0 -> pre Out;
  last_Out1 = 0 -> pre Out1;

  isp = In > 0;
  isn = In < 0;
  assume C_in_not_null: (not C) or isp or isn;

  automaton SM1
    initial state State1
      let
        Out1 = 2;
        Out = 3;
      tel
      until
        if C resume State2;
    
    state State2
      let
        automaton SM2
          initial state State3
            Out1 = 1;
            until
              if C resume State4;
          
          state State4
            activate if C
              then let
                guarantee no_mod0: Out <> 0;
                Out1 = In mod Out;
              tel else Out1 = last_Out1;
            returns Out1;
            
        returns Out1;
        
        activate if C
          then Out = In;
          else Out = last_Out;
        returns Out;
        
      tel
    
  returns Out, Out1;
tel