From 555e4b0b6b10e9170676c0a3ef9b778322f3327f Mon Sep 17 00:00:00 2001 From: yoni206 Date: Fri, 5 Mar 2021 12:09:41 -0800 Subject: [PATCH] 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. --- test/unit/api/solver_black.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/test/unit/api/solver_black.cpp b/test/unit/api/solver_black.cpp index 8e67d1287..92031b447 100644 --- 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), -- 2.30.2