137   z3::expr IsMemcpy = Type == (int)FunctionType::MEMCPY;  in RandomFunctionGenerator()
138   z3::expr ExploreAlignment = IsMemcpy && kExploreAlignmentArg;  in RandomFunctionGenerator()
207   if (Solver.check() != z3::sat)  in next()
210   z3::model m = Solver.get_model();  in next()
213   const auto E = [&m](z3::expr &V) -> int {  in next()
230   z3::expr CurrentLayout =  in next()
251 z3::expr RandomFunctionGenerator::inSetConstraint(z3::expr &Variable,  in inSetConstraint()
253   z3::expr_vector Args(Variable.ctx());  in inSetConstraint()
256   return z3::mk_or(Args);  in inSetConstraint()
259 void RandomFunctionGenerator::addBoundsAndAnchors(z3::expr &Begin,  in addBoundsAndAnchors()
260                                                   z3::expr &End) {  in addBoundsAndAnchors()
269 void RandomFunctionGenerator::addLoopConstraints(const z3::expr &LoopBegin,  in addLoopConstraints()
270                                                  const z3::expr &LoopEnd,  in addLoopConstraints()
271                                                  z3::expr &LoopBlockSize,  in addLoopConstraints()