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

(declare-fun i () String)
(declare-fun x () String)
(assert (not (str.contains x "a")))
(assert (= i (str.replace_all x "a" "b" ) ))
(assert (not (= i x)))

*/

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

$ENTRY Go {
    e.Str = <LogAnd <NotEqual (e.Str)(<Repl_A_B e.Str>)><NotA e.Str>>;
}                   

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

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

NotA {
 e.x 'A' e.y = False;
 e.x = True;
}

Repl_A_B {
 e.x 'A' e.y = e.x 'B' <Repl_A_B e.y>;
 e.z = e.z;
}

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


InputFormat_0 {
 e.x1 'A' e.x2 =  False;
 e.x1 =  False;
}
*/