Skip to content

Commit aa27ab3

Browse files
committed
revert last patch
it broke build bots and perf degraded Z3 simplifies left to right first and changing the order is not a good idea it seems
1 parent 201ee95 commit aa27ab3

File tree

1 file changed

+4
-10
lines changed

1 file changed

+4
-10
lines changed

smt/expr.cpp

Lines changed: 4 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -1211,11 +1211,8 @@ expr expr::operator&&(const expr &rhs) const {
12111211
return rhs;
12121212

12131213
C(rhs);
1214-
return binop_commutative(rhs,
1215-
[](auto ctx, auto a, auto b) {
1216-
Z3_ast args[] = { a, b };
1217-
return Z3_mk_and(ctx, 2, args);
1218-
});
1214+
Z3_ast args[] = { ast(), rhs() };
1215+
return Z3_mk_and(ctx(), 2, args);
12191216
}
12201217

12211218
expr expr::operator||(const expr &rhs) const {
@@ -1230,11 +1227,8 @@ expr expr::operator||(const expr &rhs) const {
12301227
return true;
12311228

12321229
C(rhs);
1233-
return binop_commutative(rhs,
1234-
[](auto ctx, auto a, auto b) {
1235-
Z3_ast args[] = { a, b };
1236-
return Z3_mk_or(ctx, 2, args);
1237-
});
1230+
Z3_ast args[] = { ast(), rhs() };
1231+
return Z3_mk_or(ctx(), 2, args);
12381232
}
12391233

12401234
void expr::operator&=(const expr &rhs) {

0 commit comments

Comments
 (0)