[WIP] Checking in mkConst that every Number of sort Int is indeed…

… integer

src/logics/ArithLogic.cc

@@ -543,6 +543,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();

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_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();