Skip to content

Commit b8bd6c6

Browse files
committed
SMT2 back-end: CVC5 does not support lambda expressions
I wrongly asserted (in 8fdb8bb) that CVC5 supports lambda. It seemingly does not, as can also be confirmed using Z3's test https://github.com/Z3Prover/z3test/blob/master/regressions/smt2/memset.smt2.
1 parent b1b39e8 commit b8bd6c6

File tree

1 file changed

+0
-1
lines changed

1 file changed

+0
-1
lines changed

src/solvers/smt2/smt2_conv.cpp

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -119,7 +119,6 @@ smt2_convt::smt2_convt(
119119
use_array_of_bool = true;
120120
use_as_const = true;
121121
use_check_sat_assuming = true;
122-
use_lambda_for_array = true;
123122
use_datatypes = true;
124123
break;
125124

0 commit comments

Comments
 (0)