Checking that every Number of sort Int in mkConst is indeed integer

src/logics/ArithLogic.cc

@@ -351,6 +351,45 @@ namespace {
         return logic.mkPlus(std::move(args)); // TODO: Can we use non-simplifying versions of mkPlus/mkTimes?
     }
 
+    PTRef polyToPTRefSubstitution(ArithLogic & logic, PTRef var, poly_t & poly) {
+        if ((logic.hasUFs() or logic.hasArrays()) and logic.isVar(var)) {
+            if (std::ranges::any_of(poly, [&logic](auto const & term) {
+                    return term.var != PTRef_Undef and not logic.isVar(term.var);
+                })) {
+                return PTRef_Undef;
+            }
+        }
+
+        bool const hasInts = logic.hasIntegers();
+
+        {
+            poly_t polyCp;
+            poly_t & polyRef = [&]() -> auto & {
+                if (not hasInts) { return poly; }
+                polyCp = poly;
+                return polyCp;
+            }();
+            // non-const operations on poly!
+            auto coeff = polyRef.removeVar(var);
+            coeff.negate();
+            if (not coeff.isOne()) {
+                polyRef.divideBy(coeff);
+                assert(hasInts or not logic.yieldsSortInt(var));
+                if (hasInts and logic.yieldsSortInt(var)) {
+                    if (not std::ranges::all_of(polyRef, [](auto const & term) { return term.coeff.isInteger(); })) {
+                        return PTRef_Undef;
+                    }
+                }
+            }
+
+            if (hasInts) { poly = std::move(polyCp); }
+        }
+
+        PTRef val = polyToPTRef(logic, poly);
+        assert(val != PTRef_Undef);
+        return val;
+    }
+
     Logic::SubstMap collectSingleEqualitySubstitutions(ArithLogic & logic, std::vector<poly_t> & zeroPolynomials) {
         // MB: We enforce order to ensure that later-created terms are processed first.
         //     This ensures that from an equality "f(x) = x" we get a substitution "f(x) -> x" and not the other way
@@ -369,20 +408,11 @@ namespace {
         for (auto const & [var, polyIndices] : varToPolyIndices) {
             if (polyIndices.size() != 1 or var == PTRef_Undef) { continue; }
             auto index = polyIndices[0];
-            if (processedIndices.find(index) != processedIndices.end()) { continue; }
+            if (processedIndices.contains(index)) { continue; }
             auto & poly = zeroPolynomials[index];
-            if ((logic.hasUFs() or logic.hasArrays()) and logic.isVar(var)) {
-                if (std::any_of(poly.begin(), poly.end(), [&logic](auto const & term) {
-                        return term.var != PTRef_Undef and not logic.isVar(term.var);
-                    })) {
-                    continue;
-                }
-            }
-            auto coeff = poly.removeVar(var);
-            coeff.negate();
-            if (not coeff.isOne()) { poly.divideBy(coeff); }
-            PTRef val = polyToPTRef(logic, poly);
-            substitutions.insert(var, val);
+            PTRef sub = polyToPTRefSubstitution(logic, var, poly);
+            if (sub == PTRef_Undef) { continue; }
+            substitutions.insert(var, sub);
             processedIndices.insert(index);
         }
         // Remove processed polynomials
@@ -443,20 +473,12 @@ lbool ArithLogic::arithmeticElimination(vec<PTRef> const & top_level_arith, Subs
             // Already have a substitution for this variable; skip this equality, let the main loop deal with this
             continue;
         }
-        if ((logic.hasUFs() or logic.hasArrays()) and logic.isVar(var)) {
-            if (std::any_of(poly.begin(), poly.end(), [&logic](auto const & term) {
-                    return term.var != PTRef_Undef and not logic.isVar(term.var);
-                })) {
-                continue;
-            }
-        }
 
-        auto coeff = poly.removeVar(var);
-        coeff.negate();
-        if (not coeff.isOne()) { poly.divideBy(coeff); }
-        PTRef val = polyToPTRef(logic, poly);
+        PTRef sub = polyToPTRefSubstitution(logic, var, poly);
+        if (sub == PTRef_Undef) { continue; }
+
         assert(not out_substitutions.has(var));
-        out_substitutions.insert(var, val);
+        out_substitutions.insert(var, sub);
     }
     // To simplify this method, we do not try to detect a conflict here, so result is always l_Undef
     return l_Undef;
@@ -543,6 +565,7 @@ PTRef ArithLogic::mkNeg(PTRef tr) {
 }
 
 PTRef ArithLogic::mkConst(SRef sort, Number const & c) {
+    assert(sort == sort_REAL or c.isInteger());
     std::string str = c.get_str(); // MB: I cannot store c.get_str().c_str() directly, since that is a pointer
                                    // inside temporary object -> crash.
     char const * val = str.c_str();

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 {

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
 

test/regression/base/QF_LIA/regression/lia_nosubst.smt2

@@ -0,0 +1,9 @@
+(set-logic QF_LIA)
+(declare-fun x () Int)
+(declare-fun y () Int)
+(declare-fun a () Bool)
+
+(assert (= (* 3 x) (* 4 y)))
+(assert (=> a (= x 1)))
+(assert (=> (not a) (= x 1)))
+(check-sat)

test/regression/base/QF_LIA/regression/lia_nosubst.smt2.expected.out

@@ -0,0 +1 @@
+unsat

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){

test/unit/test_Substitutions.cc

@@ -61,6 +61,27 @@ TEST_F(LIASubstitutionsRegression, test_LIAsubstitution) {
     ASSERT_EQ(res, s_False);
 }
 
+TEST_F(LIASubstitutionsRegression, test_LIANosubstitution) {
+    auto const osmt = getLIAOsmt();
+    auto & mainSolver = osmt->getMainSolver();
+    auto & lialogic = osmt->getLIALogic();
+    PTRef x = lialogic.mkIntVar("x");
+    PTRef y = lialogic.mkIntVar("y");
+    PTRef three = lialogic.mkIntConst(3);
+    PTRef four = lialogic.mkIntConst(4);
+    PTRef eq = lialogic.mkEq(lialogic.mkTimes(three, x), lialogic.mkTimes(four, y));
+    PTRef a = lialogic.mkBoolVar("a");
+    PTRef conj = lialogic.mkAnd(
+            lialogic.mkImpl(a, lialogic.mkEq(x, lialogic.getTerm_IntOne())),
+            lialogic.mkImpl(lialogic.mkNot(a), lialogic.mkEq(x, lialogic.getTerm_IntOne()))
+            );
+    PTRef fla = lialogic.mkAnd(conj, eq);
+    // 3x = 4y  AND (a => x=1) AND (~a => x=1)
+    mainSolver.insertFormula(fla);
+    auto res = mainSolver.check();
+    ASSERT_EQ(res, s_False);
+}
+
 TEST_F(LIASubstitutionsRegression, test_InconsistentSubstitutions) {
     auto const osmt = getLIAOsmt();
     auto & lialogic = osmt->getLIALogic();