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

(declare-fun x () String)
(assert (str.contains (str.replace_all x "AB" "") "CA"))
(assert (not (str.contains x "CAB")) )
(assert (not (str.contains x "CA")) )

*/

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

$ENTRY Go {
    e.Str = <LogAnd <NCont_CAB e.Str><NCont_CA e.Str><Cont_CA <Repl_AB_ e.Str>>>;
}                   

LogAnd {
 e.X False e.y = False;
 e.z = True;
}

NCont_CA {
 e.x 'CA' e.y = False;
 e.x = True;
}

Cont_CA {
 e.x 'CA' e.y = True;
 e.x = False;
}

NCont_CAB {
 e.x 'CAB' e.y = False;
 e.x = True;
}

Repl_AB_ {
 e.x 'AB' e.y = e.x <Repl_AB_ e.y>;
 e.z = e.z;
}

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


InputFormat_0 {
 e.x1 'CA' e.x2 'CAB' e.x3 =  <LogAnd_0 () (e.x1) (e.x2) (e.x3)>;
 e.x1 'CAB' e.x2 =  <LogAnd_4 () (e.x1) (e.x2)>;
 e.x1 'CA' e.x2 =  <LogAnd_8 () (e.x1) (e.x2)>;
 e.x1 =  <LogAnd_10 () (e.x1)>;
}


LogAnd_0 {
 (e.x1) (e.x2 'AB' e.x3) (e.x4) (e.x5) =  <LogAnd_0 (e.x1 e.x2) (e.x3) (e.x4) (e.x5)>;
 (e.x1) (e.x2) (e.x3 'AB' e.x4) (e.x5) =  <LogAnd_1 (e.x1 e.x2) (e.x3) (e.x4) (e.x5)>;
 (e.x1) (e.x2) (e.x3) (e.x4) =  <LogAnd_3 (e.x1 e.x2) (e.x3) () (e.x4)>;
}


LogAnd_1 {
 (e.x1) (e.x2) (e.x3 'AB' e.x4) (e.x5) =  <LogAnd_1 (e.x1) (e.x2 e.x3) (e.x4) (e.x5)>;
 (e.x1) (e.x2) (e.x3) (e.x4) =  <LogAnd_2 (e.x1) (e.x2 e.x3) () (e.x4)>;
}


LogAnd_2 {
 (e.x1) (e.x2) (e.x3) (e.x4 'AB' e.x5) =  <LogAnd_2 (e.x1) (e.x2) (e.x3 e.x4) (e.x5)>;
 (e.x1) (e.x2) (e.x3) (e.x4) =  False;
}


LogAnd_3 {
 (e.x1) (e.x2) (e.x3) (e.x4 'AB' e.x5) =  <LogAnd_3 (e.x1) (e.x2) (e.x3 e.x4) (e.x5)>;
 (e.x1) (e.x2) (e.x3) (e.x4) =  False;
}


LogAnd_4 {
 (e.x1) (e.x2 'AB' e.x3) (e.x4) =  <LogAnd_4 (e.x1 e.x2) (e.x3) (e.x4)>;
 (e.x1) (e.x2) (e.x3) =  <LogAnd_5 (e.x1 e.x2) () (e.x3)>;
}


LogAnd_5 {
 (e.x1) (e.x2) (e.x3 'AB' e.x4) =  <LogAnd_5 (e.x1) (e.x2 e.x3) (e.x4)>;
 (e.x1) ('A' e.x2) (e.x3) =  False;
 (e.x1) () ('A' e.x2) =  False;
 (e.x1) (e.x2 'CA' e.x3) (e.x4) =  False;
 (e.x1) (e.x2 'C') ('A' e.x3) =  False;
 (e.x1) (e.x2) ('CA' e.x3) =  False;
 (e.x1) (e.x2) (e.x3 'CA' e.x4) =  False;
 (e.x1) (e.x2) (e.x3) =  False;
}


LogAnd_6 {
 (e.x1) (e.x2 'AB' e.x3) (e.x4) =  <LogAnd_6 (e.x1 e.x2) (e.x3) (e.x4)>;
 (e.x1) (e.x2) (e.x3) =  <LogAnd_7 (e.x1 e.x2) () (e.x3)>;
}


LogAnd_7 {
 (e.x1) (e.x2) (e.x3 'AB' e.x4) =  <LogAnd_7 (e.x1) (e.x2 e.x3) (e.x4)>;
 (e.x1 'CA' e.x2) (e.x3) (e.x4) =  False;
 (e.x1) ('A' e.x2) (e.x3) =  False;
 (e.x1) () ('A' e.x2) =  False;
 (e.x1) (e.x2 'CA' e.x3) (e.x4) =  False;
 (e.x1) (e.x2 'C') ('A' e.x3) =  False;
 (e.x1) (e.x2) ('CA' e.x3) =  False;
 (e.x1) (e.x2) (e.x3 'CA' e.x4) =  False;
 (e.x1) (e.x2) (e.x3) =  False;
}


LogAnd_8 {
 (e.x1) (e.x2 'AB' e.x3) (e.x4) =  <LogAnd_8 (e.x1 e.x2) (e.x3) (e.x4)>;
 (e.x1) (e.x2) (e.x3 'AB' e.x4) =  <LogAnd_9 (e.x1 e.x2) (e.x3) (e.x4)>;
 (e.x1) () (e.x2) =  False;
 (e.x1) (e.x2) (e.x3) =  False;
}


LogAnd_9 {
 (e.x1) (e.x2) (e.x3 'AB' e.x4) =  <LogAnd_9 (e.x1) (e.x2 e.x3) (e.x4)>;
 (e.x1) (e.x2) (e.x3) =  False;
}


LogAnd_10 {
 (e.x1) (e.x2 'AB' e.x3) =  <LogAnd_10 (e.x1 e.x2) (e.x3)>;
 (e.x1) (e.x2) =  False;
}
*/