diff --git a/src/tsolvers/lasolver/LASolver.cc b/src/tsolvers/lasolver/LASolver.cc index 1d11eaea0..7fd19ced3 100644 --- a/src/tsolvers/lasolver/LASolver.cc +++ b/src/tsolvers/lasolver/LASolver.cc @@ -776,7 +776,7 @@ PTRef LASolver::interpolateUsingEngine(FarkasInterpolator & interpolator) const auto itpAlgorithm = config.getLRAInterpolationAlgorithm(); if (itpAlgorithm == itp_lra_alg_strong) { return interpolator.getFarkasInterpolant(); } else if (itpAlgorithm == itp_lra_alg_weak) { return interpolator.getDualFarkasInterpolant(); } - else if (itpAlgorithm == itp_lra_alg_factor) { return interpolator.getFlexibleInterpolant(Real(config.getLRAStrengthFactor())); } + else if (itpAlgorithm == itp_lra_alg_factor) { assert(not logic.hasIntegers()); return interpolator.getFlexibleInterpolant(Real(config.getLRAStrengthFactor())); } else if (itpAlgorithm == itp_lra_alg_decomposing_strong) { return interpolator.getDecomposedInterpolant(); } else if (itpAlgorithm == itp_lra_alg_decomposing_weak) { return interpolator.getDualDecomposedInterpolant(); } else { diff --git a/src/tsolvers/lasolver/LIAInterpolator.h b/src/tsolvers/lasolver/LIAInterpolator.h index 50280c1df..587fb032f 100644 --- a/src/tsolvers/lasolver/LIAInterpolator.h +++ b/src/tsolvers/lasolver/LIAInterpolator.h @@ -22,6 +22,9 @@ struct LAExplanations { class LIAInterpolator : public FarkasInterpolator { public: LIAInterpolator(ArithLogic & logic, LAExplanations liaExplanations); + + // not implemented for integers + PTRef getFlexibleInterpolant(Real strengthFactor) = delete; }; } // namespace opensmt diff --git a/test/unit/test_LIAInterpolation.cc b/test/unit/test_LIAInterpolation.cc index 635cf7757..f13e34fdb 100644 --- a/test/unit/test_LIAInterpolation.cc +++ b/test/unit/test_LIAInterpolation.cc @@ -52,9 +52,10 @@ TEST_F(LIAInterpolationTest, test_InterpolationLRASat){ PTRef dualFarkasItp = interpolator.getDualFarkasInterpolant(); std::cout << logic.pp(dualFarkasItp) << std::endl; EXPECT_TRUE(verifyInterpolant(leq1, leq2, dualFarkasItp)); - PTRef halfFarkasItp = interpolator.getFlexibleInterpolant(Number(1,2)); - std::cout << logic.pp(halfFarkasItp) << std::endl; - EXPECT_TRUE(verifyInterpolant(leq1, leq2, halfFarkasItp)); + // not implemented for integers + // PTRef halfFarkasItp = interpolator.getFlexibleInterpolant(Number(1,2)); + // std::cout << logic.pp(halfFarkasItp) << std::endl; + // EXPECT_TRUE(verifyInterpolant(leq1, leq2, halfFarkasItp)); } TEST_F(LIAInterpolationTest, test_DecompositionInLIA){