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

(declare-fun o () String)
(declare-fun v () String)
(declare-fun z () String)
(assert (= o (str.replace_all z "cb" "b" ) ))
(assert (= o (str.++ v v) ))
(assert (= v (str.++ "a" z z) ))
*/

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

$ENTRY Go {(e.z)(e.v)e.o
 = <LogAnd <IsEqual (e.o)(e.v e.v)><IsEqual (e.v)('a' e.z e.z)><IsEqual (e.o)(<Repl_cb_b e.z>)>>;
}

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

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

Repl_cb_b {
    e.X 'cb' e.Y = e.X 'b'<Repl_cb_b e.Y>;
    e.Z = e.Z;
}


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


InputFormat_0 {
 ('a' e.x1 'cb' e.x2 e.x1 'cb' e.x2 'a' e.x1 'cb' e.x2 e.x1 'cb' e.x2) (e.x3) (e.x4) =  False;
 ('a' e.x1 e.x1 'a' e.x1 e.x1) (e.x2) (e.x1) =  False;
 (e.x1 e.x1) (e.x1) (e.x2) =  False;
 (e.x1) (e.x2) (e.x3) =  False;
}
*/