Skip to content

Commit a64229c

Browse files
committed
CVC5 support floating-point theory
Set use_FPA_theory to true for this solver.
1 parent 55a26d4 commit a64229c

File tree

1 file changed

+1
-0
lines changed

1 file changed

+1
-0
lines changed

src/solvers/smt2/smt2_conv.cpp

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -116,6 +116,7 @@ smt2_convt::smt2_convt(
116116

117117
case solvert::CVC5:
118118
logic = "ALL";
119+
use_FPA_theory = true;
119120
use_array_of_bool = true;
120121
use_as_const = true;
121122
use_check_sat_assuming = true;

0 commit comments

Comments
 (0)