Searched refs:toZ3Expr (Results 1 – 1 of 1) sorted by relevance
195 static const Z3Expr &toZ3Expr(const SMTExpr &E) { in toZ3Expr() function300 auto It = CachedExprs.insert(toZ3Expr(Exp)); in newExprRef()418 toZ3Expr(*RHS).AST))); in mkBVOr()476 Z3_ast Args[2] = {toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST}; in mkAnd()481 Z3_ast Args[2] = {toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST}; in mkOr()488 toZ3Expr(*RHS).AST))); in mkEqual()521 toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST))); in mkFPMul()529 toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST))); in mkFPDiv()543 toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST))); in mkFPAdd()551 toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST))); in mkFPSub()[all …]