SMT2 parser: Do not add non-linear symbols for linear Int arith logics. (#5787)

This enables more strict handling of operators div, mod and abs
for Integer arithmetic logics.

More strict handling for '/' for Real arithmetic logics is more involved
and should be done in the parser -- instead at solving time, like is
currently done for checking that the application * is in the linear
fragment. The latter should be checked in the parser, too.
This is postponed to a later PR.

1 files changed, 6 insertions, 3 deletions

diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 36703fd6d..0c67299ab 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -550,9 +550,12 @@ Command* Smt2::setLogic(std::string name, bool fromCommand)
     if(d_logic.areIntegersUsed()) {
       defineType("Int", d_solver->getIntegerSort(), true, true);
       addArithmeticOperators();
-      addOperator(api::INTS_DIVISION, "div");
-      addOperator(api::INTS_MODULUS, "mod");
-      addOperator(api::ABS, "abs");
+      if (!d_logic.isLinear())
+      {
+        addOperator(api::INTS_DIVISION, "div");
+        addOperator(api::INTS_MODULUS, "mod");
+        addOperator(api::ABS, "abs");
+      }
       addIndexedOperator(api::DIVISIBLE, api::DIVISIBLE, "divisible");
     }