/*
The given program represents the following SMT-model:

(declare-fun x () String)
(assert (not (str.contains (str.replace_all x "bbb" "cb") "a"))
(assert (str.contains x "ca") )

*/

/***********************************************/
/*             initial program                 */
/***********************************************/

$ENTRY Go {e.c
 = <LogAnd <Cont_ca e.c><NCont_a <Repl_bbb_cb e.c>>>;
}

LogAnd {
    e.X False e.Y = False;
    e.Z = True;
}

NCont_a {
    e.X 'a' e.Y = False;
    e.Z = True;
}

Repl_bbb_cb {
     e.X 'bbb' e.Y = e.X 'cb'<Repl_bbb_cb e.Y>;
     e.Z = e.Z;
}

Cont_ca {
    e.X 'ca' e.Y = True;
    e.Z = False;
}

/***********************************************/
/*          residual program                   */
/***********************************************/
/*
$ENTRY Go {
 e.x1 =  <InputFormat_0 e.x1>;
}


InputFormat_0 {
 e.x1 'ca' e.x2 =  <LogAnd_0 () (e.x1) (e.x2)>;
 e.x1 =  <LogAnd_2 () (e.x1)>;
}


LogAnd_0 {
 (e.x1) (e.x2 'bbb' e.x3) (e.x4) =  <LogAnd_0 (e.x1 e.x2 'cb') (e.x3) (e.x4)>;
 (e.x1) (e.x2) (e.x3 'bbb' e.x4) =  <LogAnd_1 (e.x1 e.x2) (e.x3) () (e.x4)>;
 (e.x1 'a' e.x2) (e.x3) (e.x4) =  False;
 (e.x1) ('a' e.x2) (e.x3) =  False;
 (e.x1) (e.x2 'a' e.x3) (e.x4) =  False;
 (e.x1) (e.x2) (e.x3) =  False;
}


LogAnd_1 {
 (e.x1) (e.x2) (e.x3) (e.x4 'bbb' e.x5) =  <LogAnd_1 (e.x1) (e.x2) (e.x3 e.x4 'cb') (e.x5)>;
 (e.x1 'a' e.x2) (e.x3) (e.x4) (e.x5) =  False;
 (e.x1) (e.x2) (e.x3) (e.x4) =  False;
}


LogAnd_2 {
 (e.x1) (e.x2 'bbb' e.x3) =  <LogAnd_2 (e.x1 e.x2 'cb') (e.x3)>;
 (e.x1 'a' e.x2) (e.x3) =  False;
 (e.x1) ('a' e.x2) =  False;
 (e.x1) (e.x2 'a' e.x3) =  False;
 (e.x1) (e.x2) =  False;
}
*/