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

(declare-fun x () String)
(assert (= (str.replace_all x "a" "b") (str.replace_all x "ba" "cc")))
(assert (str.contains x "ac") )

*/

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

$ENTRY Go {(e.b)
 = <LogAnd <IsEqual (<Repl_a_b e.b>)(<Repl_ba_cc e.b>)><Cont_ac e.b>>;
}

IsEqual {
    (e.x)(e.x) = True;
    (e.x)(e.y) = False;
}

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

Cont_ac {
    e.X 'ac' e.X1 = True;
    e.Y  = False;
}

Repl_a_b {
    e.X 'a' e.Y = e.X 'b'<Repl_a_b e.Y>;
    e.X = e.X;
}

Repl_ba_cc {
    e.X 'ba' e.Y = e.X 'cc'<Repl_ba_cc e.Y>;
    e.X = e.X;
}

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


InputFormat_0 {
 e.x1 'bac' e.x2 =  False;
 e.x1 'ba' e.x2 'ac' e.x3 =  False;
 e.x1 'ba' e.x2 =  False;
 e.x1 'ac' e.x2 'ba' e.x3 =  False;
 e.x1 'a' e.x2 'ac' e.x3 'ba' e.x4 =  False;
 e.x1 'a' e.x2 'bac' e.x3 =  False;
 e.x1 'a' e.x2 'ba' e.x3 'ac' e.x4 =  False;
 e.x1 'a' e.x2 'ba' e.x3 =  False;
 e.x1 'ac' e.x2 =  False;
 e.x1 'a' e.x2 'ac' e.x3 =  False;
 e.x1 'a' e.x2 =  False;
 e.x1 =  False;
}
*/