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

(declare-fun v () String)
(declare-fun a () String)
(declare-fun q () String)
(assert (= q (str.replace_all v "ac" "cabba")) )
(assert (= q (str.++ v a)) )
(assert (str.contains a "b") )

*/

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

$ENTRY Go {(e.v)(e.a)e.q
 = <LogAnd <Cont_b e.a><IsEqual (e.q)(e.v e.a)><IsEqual (e.q)(<Repl_ac_cabba e.v>)>>;
}

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

LogAnd {
    False e.Y = False;
    True = True;
    True e.Z = <LogAnd e.Z>;
}

Cont_b {
   e.X 'b' e.Y = True;
   e.Z  = False;
}

Repl_ac_cabba {
    e.X 'ac' e.Y = e.X 'cabba'<Repl_ac_cabba e.Y>;
    e.Z = e.Z;
}


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


InputFormat_0 {
 (e.x1 'b' e.x2) (e.x3 'ac' e.x4 e.x1 'b' e.x2) (e.x5) =  False;
 (e.x1 'b' e.x2) (e.x3 e.x1 'b' e.x2) (e.x3) =  False;
 (e.x1 'b' e.x2) (e.x3) (e.x4) =  False;
 (e.x1) (e.x2) (e.x3) =  False;
}
*/