Skip to content

Commit a8a325f

Browse files
committed
SMT2 backend: use FPA theory with --cprover-smt2
This enables the use of the FloatingPoint theory when using cprover_smt2. The resulting SMT-LIB files are much smaller, and easier to read.
1 parent 5b9858f commit a8a325f

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
@@ -85,6 +85,7 @@ smt2_convt::smt2_convt(
8585
break;
8686

8787
case solvert::CPROVER_SMT2:
88+
use_FPA_theory = true;
8889
use_array_of_bool = true;
8990
use_as_const = true;
9091
use_check_sat_assuming = true;

0 commit comments

Comments
 (0)