Set logic in interpolation unit test. (#6067)

The logic QF_LIA was not set in the api interpolation test.
Setting it brings the solving time from ~37s to ~2s.
Also, a comment is fixed.

diff --git a/test/unit/api/solver_black.cpp b/test/unit/api/solver_black.cpp
index 8e67d128790b849626cff8b1507da650257ca3a3..92031b4476573ce229fecdd8264ed69c36466289 100644 (file)
--- a/test/unit/api/solver_black.cpp
+++ b/test/unit/api/solver_black.cpp
@@ -1269,6 +1269,7 @@ TEST_F(TestApiBlackSolver, getInfo)
 
 TEST_F(TestApiBlackSolver, getInterpolant)
 {
+  d_solver.setLogic("QF_LIA");
   d_solver.setOption("produce-interpols", "default");
   d_solver.setOption("incremental", "false");
 
@@ -1282,7 +1283,7 @@ TEST_F(TestApiBlackSolver, getInterpolant)
   d_solver.assertFormula(
       d_solver.mkTerm(GT, d_solver.mkTerm(PLUS, x, y), zero));
   d_solver.assertFormula(d_solver.mkTerm(LT, x, zero));
-  // Conjecture for interpolation: y + z > 0 /\ z < 0
+  // Conjecture for interpolation: y + z > 0 \/ z < 0
   Term conj =
       d_solver.mkTerm(OR,
                       d_solver.mkTerm(GT, d_solver.mkTerm(PLUS, y, z), zero),