From: Alex Ozdemir <aozdemir@hmc.edu>
Date: Sat, 22 Feb 2020 00:16:19 +0000 (-0800)
Subject: Switch to th_lira.plf (#3741)
X-Git-Tag: cvc5-1.0.0~3620
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=a98cd6d50308d1dde1086f0c1502e022bd30ba1b;p=cvc5.git

Switch to th_lira.plf (#3741)

Switches arith_proof.cpp from th_lra to th_lira.

Changes:

Eliminate the d_realMode hack.
instead: modify printOwnedTermAsType prints as integers OR
reals, depending on expectedType.
simultaneously: write printOwnedTermAsType more concisely
also: reimplement printOwnedSort.
Change to the LIRA axioms:
Because they reason about bound types using side conditions, we
no longer need to worry about choosing the correct strictness for
our axiom.
This allows us to cut out a lot of code, rewriting & shrinking
printTheoryLemmaProof.
They also have different names.
This requires us to change a lot of string literals
enable proof-checking for many tests.
---

diff --git a/proofs/signatures/CMakeLists.txt b/proofs/signatures/CMakeLists.txt
index 86474585c..698fa37fe 100644
--- a/proofs/signatures/CMakeLists.txt
+++ b/proofs/signatures/CMakeLists.txt
@@ -16,7 +16,7 @@ set(core_signature_files
     th_bv_rewrites.plf
     th_real.plf
     th_int.plf
-    th_lra.plf
+    th_lira.plf
 )
 
 set(CORE_SIGNATURES "")
diff --git a/src/proof/arith_proof.cpp b/src/proof/arith_proof.cpp
index ee7bf5f99..7deb22d48 100644
--- a/src/proof/arith_proof.cpp
+++ b/src/proof/arith_proof.cpp
@@ -19,7 +19,9 @@
 #include <memory>
 #include <stack>
 
+#include "base/check.h"
 #include "expr/node.h"
+#include "expr/type_checker_util.h"
 #include "proof/proof_manager.h"
 #include "proof/theory_proof.h"
 #include "theory/arith/constraint_forward.h"
@@ -656,7 +658,7 @@ Node ProofArith::toStreamRecLFSC(std::ostream& out,
 }
 
 ArithProof::ArithProof(theory::arith::TheoryArith* arith, TheoryProofEngine* pe)
-  : TheoryProof(arith, pe), d_recorder(), d_realMode(false)
+  : TheoryProof(arith, pe), d_recorder()
 {
   arith->setProofRecorder(&d_recorder);
 }
@@ -668,7 +670,6 @@ void ArithProof::registerTerm(Expr term) {
 
   if (term.getType().isReal() && !term.getType().isInteger()) {
     Debug("pf::arith") << "Entering real mode" << std::endl;
-    d_realMode = true;
   }
 
   if (term.isVariable() && !ProofManager::getSkolemizationManager()->isSkolem(term)) {
@@ -693,7 +694,12 @@ void LFSCArithProof::printOwnedTermAsType(Expr term,
 
   // !d_realMode <--> term.getType().isInteger()
 
-  Assert(theory::Theory::theoryOf(term) == theory::THEORY_ARITH);
+  Assert (theory::Theory::theoryOf(term) == theory::THEORY_ARITH);
+  std::ostringstream closing;
+  if (!expectedType.isNull() && !expectedType.isInteger() && term.getType().isInteger()) {
+    os << "(term_int_to_real ";
+    closing << ")";
+  }
   switch (term.getKind())
   {
     case kind::CONST_RATIONAL:
@@ -704,14 +710,16 @@ void LFSCArithProof::printOwnedTermAsType(Expr term,
       const Rational& r = term.getConst<Rational>();
       bool neg = (r < 0);
 
-      os << (!d_realMode ? "(a_int " : "(a_real ");
+      os << (term.getType().isInteger() ? "(a_int " : "(a_real ");
+      closing << ") ";
 
       if (neg)
       {
         os << "(~ ";
+        closing << ")";
       }
 
-      if (!d_realMode)
+      if (term.getType().isInteger())
       {
         os << r.abs();
       }
@@ -720,155 +728,90 @@ void LFSCArithProof::printOwnedTermAsType(Expr term,
         printRational(os, r.abs());
       }
 
-      if (neg)
-      {
-        os << ") ";
-      }
-
-      os << ") ";
-      return;
-    }
-
-    case kind::UMINUS:
-    {
-      Assert(term.getNumChildren() == 1);
-      Assert(term.getType().isInteger() || term.getType().isReal());
-      os << (!d_realMode ? "(u-_Int " : "(u-_Real ");
-      d_proofEngine->printBoundTerm(term[0], os, map);
-      os << ") ";
-      return;
+      break;
     }
 
     case kind::PLUS:
-    {
-      Assert(term.getNumChildren() >= 2);
-
-      std::stringstream paren;
-      for (unsigned i = 0; i < term.getNumChildren() - 1; ++i)
-      {
-        os << (!d_realMode ? "(+_Int " : "(+_Real ");
-        d_proofEngine->printBoundTerm(term[i], os, map);
-        os << " ";
-        paren << ") ";
-      }
-
-      d_proofEngine->printBoundTerm(term[term.getNumChildren() - 1], os, map);
-      os << paren.str();
-      return;
-    }
-
     case kind::MINUS:
+    case kind::MULT:
+    case kind::DIVISION:
+    case kind::DIVISION_TOTAL:
     {
-      Assert(term.getNumChildren() >= 2);
+      Assert(term.getNumChildren() >= 1);
+      TypeNode ty = Node::fromExpr(term).getType();
 
-      std::stringstream paren;
+      std::string lfscFunction = getLfscFunction(term);
       for (unsigned i = 0; i < term.getNumChildren() - 1; ++i)
       {
-        os << (!d_realMode ? "(-_Int " : "(-_Real ");
-        d_proofEngine->printBoundTerm(term[i], os, map);
+        os << "(" << lfscFunction << " ";
+        closing << ")";
+        d_proofEngine->printBoundTerm(term[i], os, map, ty);
         os << " ";
-        paren << ") ";
       }
 
-      d_proofEngine->printBoundTerm(term[term.getNumChildren() - 1], os, map);
-      os << paren.str();
-      return;
+      d_proofEngine->printBoundTerm(term[term.getNumChildren() - 1], os, map, ty);
+      break;
     }
 
-    case kind::MULT:
+    case kind::UMINUS:
     {
-      Assert(term.getNumChildren() >= 2);
-
-      std::stringstream paren;
-      for (unsigned i = 0; i < term.getNumChildren() - 1; ++i)
-      {
-        os << (!d_realMode ? "(*_Int " : "(*_Real ");
-        d_proofEngine->printBoundTerm(term[i], os, map);
-        os << " ";
-        paren << ") ";
-      }
-
-      d_proofEngine->printBoundTerm(term[term.getNumChildren() - 1], os, map);
-      os << paren.str();
-      return;
+      Assert(term.getNumChildren() == 1);
+      os << "(" << getLfscFunction(term) << " ";
+      closing << ")";
+      d_proofEngine->printBoundTerm(term[0], os, map, Node::fromExpr(term).getType());
+      break;
     }
 
-    case kind::DIVISION:
-    case kind::DIVISION_TOTAL:
+    case kind::GT:
+    case kind::GEQ:
+    case kind::LT:
+    case kind::LEQ:
     {
-      Assert(term.getNumChildren() >= 2);
+      Assert(term.getNumChildren() == 2);
+      Assert(term.getType().isBoolean());
 
-      std::stringstream paren;
-      for (unsigned i = 0; i < term.getNumChildren() - 1; ++i)
-      {
-        os << (!d_realMode ? "(/_Int " : "(/_Real ");
-        d_proofEngine->printBoundTerm(term[i], os, map);
-        os << " ";
-        paren << ") ";
-      }
+      std::string lfscFunction = getLfscFunction(term);
+      TypeNode realType = NodeManager::currentNM()->realType();
 
-      d_proofEngine->printBoundTerm(term[term.getNumChildren() - 1], os, map);
-      os << paren.str();
-      return;
-    }
+      os << "(" << lfscFunction << " ";
+      closing << ")";
 
-    case kind::GT:
-      Assert(term.getNumChildren() == 2);
-      os << (!d_realMode ? "(>_Int " : "(>_Real ");
       d_proofEngine->printBoundTerm(term[0], os, map);
       os << " ";
-      d_proofEngine->printBoundTerm(term[1], os, map);
-      os << ") ";
-      return;
-
-    case kind::GEQ:
+      d_proofEngine->printBoundTerm(term[1], os, map, realType);
+      break;
+    }
+    case kind::EQUAL:
+    {
+      Assert(term.getType().isBoolean());
       Assert(term.getNumChildren() == 2);
-      os << (!d_realMode ? "(>=_Int " : "(>=_Real ");
-      d_proofEngine->printBoundTerm(term[0], os, map);
-      os << " ";
-      d_proofEngine->printBoundTerm(term[1], os, map);
-      os << ") ";
-      return;
 
-    case kind::LT:
-      Assert(term.getNumChildren() == 2);
-      os << (!d_realMode ? "(<_Int " : "(<_Real ");
-      d_proofEngine->printBoundTerm(term[0], os, map);
-      os << " ";
-      d_proofEngine->printBoundTerm(term[1], os, map);
-      os << ") ";
-      return;
+      TypeNode eqType = equalityType(term[0], term[1]);
 
-    case kind::LEQ:
-      Assert(term.getNumChildren() == 2);
-      os << (!d_realMode ? "(<=_Int " : "(<=_Real ");
-      d_proofEngine->printBoundTerm(term[0], os, map);
-      os << " ";
-      d_proofEngine->printBoundTerm(term[1], os, map);
-      os << ") ";
-      return;
+      os << "(= " << eqType << " ";
+      closing << ")";
+
+      d_proofEngine->printBoundTerm(term[0], os, map, eqType);
+      d_proofEngine->printBoundTerm(term[1], os, map, eqType);
+      break;
+    }
 
     case kind::VARIABLE:
     case kind::SKOLEM:
       os << CVC4_ARITH_VAR_TERM_PREFIX << ProofManager::sanitize(term);
-      return;
+      break;
 
     default:
       Debug("pf::arith") << "Default printing of term: " << term << std::endl;
       os << term;
-      return;
+      break;
   }
+  os << closing.str();
 }
 
 void LFSCArithProof::printOwnedSort(Type type, std::ostream& os) {
   Debug("pf::arith") << "Arith print sort: " << type << std::endl;
-
-  if (type.isInteger() && d_realMode) {
-    // If in "real mode", don't use type Int for, e.g., equality.
-    os << "Real";
-  } else {
-    os << type;
-  }
+  os << type;
 }
 
 std::string LFSCArithProof::getLfscFunction(const Node & n) {
@@ -960,7 +903,7 @@ void LFSCArithProof::printLinearPolynomialNormalizer(std::ostream& o,
       {
         if (i < nchildren - 1)
         {
-          o << "\n      (pn_+ _ _ _ _ _ ";
+          o << "\n      (is_aff_+ _ _ _ _ _ ";
         }
         printLinearMonomialNormalizer(o, n[i]);
       }
@@ -976,10 +919,8 @@ void LFSCArithProof::printLinearPolynomialNormalizer(std::ostream& o,
       break;
     }
     default:
-#ifdef CVC4_ASSERTIONS
       Unreachable() << "Invalid operation " << n.getKind()
                     << " in linear polynomial";
-#endif  // CVC4_ASSERTIONS
       break;
   }
 }
@@ -990,15 +931,13 @@ void LFSCArithProof::printLinearMonomialNormalizer(std::ostream& o,
   switch (n.getKind())
   {
     case kind::MULT: {
-#ifdef CVC4_ASSERTIONS
       Assert((n[0].getKind() == kind::CONST_RATIONAL
               && (n[1].getKind() == kind::VARIABLE
                   || n[1].getKind() == kind::SKOLEM)))
           << "node " << n << " is not a linear monomial"
           << " " << n[0].getKind() << " " << n[1].getKind();
-#endif  // CVC4_ASSERTIONS
 
-      o << "\n        (pn_mul_c_L _ _ _ ";
+      o << "\n        (is_aff_mul_c_L _ _ _ ";
       printConstRational(o, n[0]);
       o << " ";
       printVariableNormalizer(o, n[1]);
@@ -1007,7 +946,7 @@ void LFSCArithProof::printLinearMonomialNormalizer(std::ostream& o,
     }
     case kind::CONST_RATIONAL:
     {
-      o << "\n        (pn_const ";
+      o << "\n        (is_aff_const ";
       printConstRational(o, n);
       o << ")";
       break;
@@ -1020,10 +959,8 @@ void LFSCArithProof::printLinearMonomialNormalizer(std::ostream& o,
       break;
     }
     default:
-#ifdef CVC4_ASSERTIONS
       Unreachable() << "Invalid operation " << n.getKind()
                     << " in linear monomial";
-#endif  // CVC4_ASSERTIONS
       break;
   }
 }
@@ -1037,9 +974,17 @@ void LFSCArithProof::printConstRational(std::ostream& o, const Node& n)
 
 void LFSCArithProof::printVariableNormalizer(std::ostream& o, const Node& n)
 {
+  std::ostringstream msg;
   Assert(n.getKind() == kind::VARIABLE || n.getKind() == kind::SKOLEM)
       << "Invalid variable kind " << n.getKind() << " in linear monomial";
-  o << "(pn_var " << n << ")";
+  if (n.getType().isInteger()) {
+    o << "(is_aff_var_int ";
+  } else if (n.getType().isReal()) {
+    o << "(is_aff_var_real ";
+  } else {
+    Unreachable();
+  }
+  o << n << ")";
 }
 
 void LFSCArithProof::printLinearPolynomialPredicateNormalizer(std::ostream& o,
@@ -1048,12 +993,11 @@ void LFSCArithProof::printLinearPolynomialPredicateNormalizer(std::ostream& o,
   Assert(n.getKind() == kind::GEQ)
       << "can only print normalization witnesses for (>=) nodes";
   Assert(n[1].getKind() == kind::CONST_RATIONAL);
-  o << "(poly_formula_norm_>= _ _ _ ";
-  o << "\n    (pn_- _ _ _ _ _ ";
+  o << "\n    (is_aff_- _ _ _ _ _ ";
   printLinearPolynomialNormalizer(o, n[0]);
-  o << "\n      (pn_const ";
+  o << "\n      (is_aff_const ";
   printConstRational(o, n[1]);
-  o << ")))";
+  o << "))";
 }
 
 std::pair<Node, std::string> LFSCArithProof::printProofAndMaybeTighten(
@@ -1075,24 +1019,16 @@ std::pair<Node, std::string> LFSCArithProof::printProofAndMaybeTighten(
         Assert(nonNegBound[1].getKind() == kind::CONST_RATIONAL);
         Rational oldBound = nonNegBound[1].getConst<Rational>();
         Integer newBound = -(oldBound.ceiling() - 1);
+        // Since the arith theory rewrites bounds to be purely integral or
+        // purely real, mixed bounds should not appear in proofs
+        AlwaysAssert(oldBound.isIntegral()) << "Mixed int/real bound in arith proof";
         pfOfPossiblyTightenedPredicate
-            << "("
-            << (oldBound.isIntegral() ? "tighten_not_>=_IntInt"
-                                      : "tighten_not_>=_IntReal")
+            << "(tighten_not_>=_IntInt"
             << " _ _ _ _ ("
-            << (oldBound.isIntegral()
-                    ? "check_neg_of_greatest_integer_below_int "
-                    : "check_neg_of_greatest_integer_below ");
+            << "check_neg_of_greatest_integer_below_int ";
         printInteger(pfOfPossiblyTightenedPredicate, newBound);
         pfOfPossiblyTightenedPredicate << " ";
-        if (oldBound.isIntegral())
-        {
-          printInteger(pfOfPossiblyTightenedPredicate, oldBound.ceiling());
-        }
-        else
-        {
-          printRational(pfOfPossiblyTightenedPredicate, oldBound);
-        }
+        printInteger(pfOfPossiblyTightenedPredicate, oldBound.ceiling());
         pfOfPossiblyTightenedPredicate << ") " << ProofManager::getLitName(bound.negate(), "") << ")";
         Node newLeft = (theory::arith::Polynomial::parsePolynomial(nonNegBound[0]) * -1).getNode();
         Node newRight = NodeManager::currentNM()->mkConst(Rational(newBound));
@@ -1108,18 +1044,11 @@ std::pair<Node, std::string> LFSCArithProof::printProofAndMaybeTighten(
         Assert(nonNegBound[1].getKind() == kind::CONST_RATIONAL);
 
         Rational oldBound = nonNegBound[1].getConst<Rational>();
-        if (oldBound.isIntegral()) {
-          pfOfPossiblyTightenedPredicate << ProofManager::getLitName(bound.negate(), "");
-          return std::make_pair(bound, pfOfPossiblyTightenedPredicate.str());
-        } else {
-          Integer newBound = oldBound.ceiling();
-          pfOfPossiblyTightenedPredicate << "(tighten_>=_IntReal _ _ " <<
-            newBound << " " << ProofManager::getLitName(bound.negate(), "") << ")";
-          Node newRight = NodeManager::currentNM()->mkConst(Rational(newBound));
-          Node newTerm = NodeManager::currentNM()->mkNode(kind::GEQ, nonNegBound[0], newRight);
-          return std::make_pair(newTerm, pfOfPossiblyTightenedPredicate.str());
-        }
-        break;
+        // Since the arith theory rewrites bounds to be purely integral or
+        // purely real, mixed bounds should not appear in proofs
+        AlwaysAssert(oldBound.isIntegral()) << "Mixed int/real bound in arith proof";
+        pfOfPossiblyTightenedPredicate << ProofManager::getLitName(bound.negate(), "");
+        return std::make_pair(bound, pfOfPossiblyTightenedPredicate.str());
       }
       default: Unreachable();
     }
@@ -1136,9 +1065,14 @@ void LFSCArithProof::printTheoryLemmaProof(std::vector<Expr>& lemma,
                                            const ProofLetMap& map)
 {
   Debug("pf::arith") << "Printing proof for lemma " << lemma << std::endl;
+  if (Debug.isOn("pf::arith::printTheoryLemmaProof")) {
+    Debug("pf::arith::printTheoryLemmaProof") << "Printing proof for lemma:" << std::endl;
+    for (const auto & conjunct : lemma) {
+      Debug("pf::arith::printTheoryLemmaProof") << "  " << conjunct << std::endl;
+    }
+  }
   // Prefixes for the names of linearity witnesses
-  const char* linearityWitnessPrefix = "lp";
-  const char* linearizedProofPrefix = "pf_lp";
+  const char* linearizedProofPrefix = "pf_aff";
   std::ostringstream lemmaParen;
 
   // Construct the set of conflicting literals
@@ -1163,26 +1097,15 @@ void LFSCArithProof::printTheoryLemmaProof(std::vector<Expr>& lemma,
     const size_t nAntecedents = conflict.getNumChildren();
 
     // Print proof
-    os << "\n;; Farkas Proof" << std::endl;
-
-    // Construct witness that the literals are linear polynomials
-    os << ";  Linear Polynomial Normalization Witnesses" << std::endl;
-    for (size_t i = 0; i != nAntecedents; ++i)
-    {
-      const Node& antecedent = conflict[i];
-      const Rational farkasC = (*farkasCoefficients)[i];
-      os << "\n; " << antecedent << " w/ farkas c = " << farkasC << std::endl;
-      os << "  (@ "
-         << ProofManager::getLitName(antecedent.negate(),
-                                     linearityWitnessPrefix)
-         << " ";
-      const Node& nonneg =
-          antecedent.getKind() == kind::NOT ? antecedent[0] : antecedent;
-      printLinearPolynomialPredicateNormalizer(os, nonneg);
-      lemmaParen << ")";
+    if (Debug.isOn("pf::arith::printTheoryLemmaProof")) {
+      os << "Farkas:" << std::endl;
+      for (const auto & n : *farkasCoefficients) {
+        os << "  " << n << std::endl;
+      }
     }
 
-    // Prove linear polynomial constraints
+    // Prove affine function bounds from term bounds
+    os << "\n;; Farkas Proof ;;" << std::endl;
     os << "\n;  Linear Polynomial Proof Conversions";
     for (size_t i = 0; i != nAntecedents; ++i)
     {
@@ -1191,113 +1114,45 @@ void LFSCArithProof::printTheoryLemmaProof(std::vector<Expr>& lemma,
          << ProofManager::getLitName(antecedent.negate(), linearizedProofPrefix)
          << " ";
       lemmaParen << ")";
-      switch (conflict[i].getKind())
+      const std::pair<Node, std::string> tightened = printProofAndMaybeTighten(antecedent);
+      switch (tightened.first.getKind())
       {
         case kind::NOT:
         {
           Assert(conflict[i][0].getKind() == kind::GEQ);
-          os << "(poly_flip_not_>= _ _ "
-             << "(poly_form_not _ _ "
-             << ProofManager::getLitName(antecedent.negate(),
-                                         linearityWitnessPrefix)
-             << " " << ProofManager::getLitName(antecedent.negate(), "")
-             << "))";
+          os << "(aff_>_from_term _ _ _ _ ";
           break;
         }
         case kind::GEQ:
         {
-          os << "(poly_form _ _ "
-             << ProofManager::getLitName(antecedent.negate(),
-                                         linearityWitnessPrefix)
-             << " " << ProofManager::getLitName(antecedent.negate(), "") << ")";
+          os << "(aff_>=_from_term _ _ _ ";
           break;
         }
         default: Unreachable();
       }
+      const Node& nonNegTightened = tightened.first.getKind() == kind::NOT ? tightened.first[0] : tightened.first;
+      printLinearPolynomialPredicateNormalizer(os, nonNegTightened);
+      os << " (pf_reified_arith_pred _ _ " << tightened.second << "))";
     }
 
-    /* Combine linear polynomial constraints to derive a contradiction.
-     *
-     * The linear polynomial constraints are refered to as **antecedents**,
-     * since they are antecedents to the contradiction.
-     *
-     * The structure of the combination is a tree
-     *
-     *   (=> <=)
-     *      |
-     *      +                   0
-     *     / \
-     *    *   +                 1
-     *       / \
-     *      *   +               2
-     *         / \
-     *        *  ...            i
-     *             \
-     *              +           n-1
-     *             / \
-     *            *   (0 >= 0)
-     *
-     * Where each * is a linearized antecedant being scaled by a farkas
-     * coefficient and each + is the sum of inequalities. The tricky bit is that
-     * each antecedent can be strict (>) or relaxed (>=) and the axiom used for
-     * each * and + depends on this... The axiom for * depends on the
-     * strictness of its linear polynomial input, and the axiom for + depends
-     * on the strictness of **both** its inputs. The contradiction axiom is
-     * also a function of the strictness of its input.
-     *
-     * There are n *s and +s and we precompute
-     *    1. The strictness of the ith antecedant  (`ith_antecedent_is_strict`)
-     *    2. The strictness of the right argument of the ith sum
-     * (`ith_acc_is_strict`)
-     *    3. The strictness of the final result (`strict_contradiction`)
-     *
-     * Precomupation is helpful since
-     *    the computation is post-order,
-     *    but printing is pre-order.
-     */
-    std::vector<bool> ith_antecedent_is_strict(nAntecedents, false);
-    std::vector<bool> ith_acc_is_strict(nAntecedents, false);
-    for (int i = nAntecedents - 1; i >= 0; --i)
-    {
-      ith_antecedent_is_strict[i] = conflict[i].getKind() == kind::NOT;
-      if (i == (int)nAntecedents - 1)
-      {
-        ith_acc_is_strict[i] = false;
-      }
-      else
-      {
-        ith_acc_is_strict[i] =
-            ith_acc_is_strict[i + 1] || ith_antecedent_is_strict[i + 1];
-      }
-    }
-    bool strict_contradiction =
-        ith_acc_is_strict[0] || ith_antecedent_is_strict[0];
-
-    // Now, print the proof
+    // Now, print the proof of bottom, from affine function bounds
     os << "\n;  Farkas Combination";
-    // Choose the appropriate contradiction axiom
-    os << "\n  (lra_contra_" << (strict_contradiction ? ">" : ">=") << " _ ";
+    os << "\n  (clausify_false (bounded_aff_contra _ _";
+    lemmaParen << "))";
     for (size_t i = 0; i != nAntecedents; ++i)
     {
       const Node& lit = conflict[i];
-      const char* ante_op = ith_antecedent_is_strict[i] ? ">" : ">=";
-      const char* acc_op = ith_acc_is_strict[i] ? ">" : ">=";
-      os << "\n    (lra_add_" << ante_op << "_" << acc_op << " _ _ _ ";
-      os << "\n       (lra_mul_c_" << ante_op << " _ _ ";
+      os << "\n    (bounded_aff_add _ _ _ _ _";
+      os << "\n       (bounded_aff_mul_c _ _ _ ";
       printRational(os, (*farkasCoefficients)[i].abs());
       os << " " << ProofManager::getLitName(lit.negate(), linearizedProofPrefix)
          << ")"
          << " ; " << lit;
+      lemmaParen << ")";
     }
 
-    // The basis, at least, is always the same...
-    os << "\n    (lra_axiom_>= 0/1)";
-    std::fill_n(std::ostream_iterator<char>(os),
-                nAntecedents,
-                ')');  // close lra_add_*_*
-    os << ")";         // close lra_contra_*
-
-    os << lemmaParen.str();  // close normalizers and proof-normalizers
+    os << "\n    bounded_aff_ax_0_>=_0";
+    os << lemmaParen.str();  // Close lemma proof
   }
   else
   {
@@ -1317,10 +1172,12 @@ void LFSCArithProof::printTermDeclarations(std::ostream& os, std::ostream& paren
   {
     Expr term = *it;
     Assert(term.isVariable());
-    os << "(% " << ProofManager::sanitize(term) << " var_real\n";
+    bool isInt = term.getType().isInteger();
+    const char * var_type = isInt ? "int_var" : "real_var";
+    os << "(% " << ProofManager::sanitize(term) << " " << var_type << "\n";
     os << "(@ " << CVC4_ARITH_VAR_TERM_PREFIX << ProofManager::sanitize(term)
        << " ";
-    os << "(a_var_real " << ProofManager::sanitize(term) << ")\n";
+    os << "(term_" << var_type << " " << ProofManager::sanitize(term) << ")\n";
     paren << ")";
     paren << ")";
   }
diff --git a/src/proof/arith_proof.h b/src/proof/arith_proof.h
index 587569b1a..b889614f1 100644
--- a/src/proof/arith_proof.h
+++ b/src/proof/arith_proof.h
@@ -68,7 +68,6 @@ protected:
    */
   proof::ArithProofRecorder d_recorder;
 
-  bool d_realMode;
   theory::TheoryId getTheoryId() override;
 
  public:
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index d61203ac2..9469e7d61 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -6,9 +6,10 @@ set(regress_0_tests
   regress0/arith/arith-eq.smt2
   regress0/arith/arith-mixed-types-no-tighten.smt2
   regress0/arith/arith-mixed-types-tighten.smt2
-  regress0/arith/arith-mixed.smt2
+  regress0/arith/arith-strict-relaxed.smt2
   regress0/arith/arith-strict.smt2
   regress0/arith/arith-tighten-1.smt2
+  regress0/arith/arith-tighten-2.smt2
   regress0/arith/arith.01.cvc
   regress0/arith/arith.02.cvc
   regress0/arith/arith.03.cvc
diff --git a/test/regress/regress0/arith/arith-eq.smt2 b/test/regress/regress0/arith/arith-eq.smt2
index 661c3f242..38de29734 100644
--- a/test/regress/regress0/arith/arith-eq.smt2
+++ b/test/regress/regress0/arith/arith-eq.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --no-check-unsat-cores --no-check-proofs
+; COMMAND-LINE: --no-check-unsat-cores
 ; EXPECT: unsat
 (set-logic QF_LRA)
 
diff --git a/test/regress/regress0/arith/arith-mixed-types-no-tighten.smt2 b/test/regress/regress0/arith/arith-mixed-types-no-tighten.smt2
index a06621224..2f02c9d1e 100644
--- a/test/regress/regress0/arith/arith-mixed-types-no-tighten.smt2
+++ b/test/regress/regress0/arith/arith-mixed-types-no-tighten.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --no-check-unsat-cores --no-check-proofs
+; COMMAND-LINE: --no-check-unsat-cores
 ; EXPECT: unsat
 (set-logic QF_LIRA)
 
diff --git a/test/regress/regress0/arith/arith-mixed-types-tighten.smt2 b/test/regress/regress0/arith/arith-mixed-types-tighten.smt2
index 2f737d5c5..627118777 100644
--- a/test/regress/regress0/arith/arith-mixed-types-tighten.smt2
+++ b/test/regress/regress0/arith/arith-mixed-types-tighten.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --no-check-unsat-cores --no-check-proofs
+; COMMAND-LINE: --no-check-unsat-cores
 ; EXPECT: unsat
 (set-logic QF_LIRA)
 
diff --git a/test/regress/regress0/arith/arith-mixed.smt2 b/test/regress/regress0/arith/arith-mixed.smt2
deleted file mode 100644
index 5869a51bd..000000000
--- a/test/regress/regress0/arith/arith-mixed.smt2
+++ /dev/null
@@ -1,14 +0,0 @@
-; COMMAND-LINE: --no-check-unsat-cores --no-check-proofs
-; EXPECT: unsat
-(set-logic QF_LRA)
-
-(declare-fun x () Real)
-(declare-fun y () Real)
-(declare-fun z () Real)
-
-; Both strict and non-strict inequalities.
-(assert (< y 0))
-(assert (>= y x))
-(assert (>= y (- x)))
-
-(check-sat)
diff --git a/test/regress/regress0/arith/arith-strict-relaxed.smt2 b/test/regress/regress0/arith/arith-strict-relaxed.smt2
new file mode 100644
index 000000000..fe17aa536
--- /dev/null
+++ b/test/regress/regress0/arith/arith-strict-relaxed.smt2
@@ -0,0 +1,14 @@
+; COMMAND-LINE: --no-check-unsat-cores
+; EXPECT: unsat
+(set-logic QF_LRA)
+
+(declare-fun x () Real)
+(declare-fun y () Real)
+(declare-fun z () Real)
+
+; Both strict and non-strict inequalities.
+(assert (< y 0))
+(assert (>= y x))
+(assert (>= y (- x)))
+
+(check-sat)
diff --git a/test/regress/regress0/arith/arith-strict.smt2 b/test/regress/regress0/arith/arith-strict.smt2
index 969cfd0bb..b1477732c 100644
--- a/test/regress/regress0/arith/arith-strict.smt2
+++ b/test/regress/regress0/arith/arith-strict.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --no-check-unsat-cores --no-check-proofs
+; COMMAND-LINE: --no-check-unsat-cores
 ; EXPECT: unsat
 (set-logic QF_LRA)
 
diff --git a/test/regress/regress0/arith/arith-tighten-1.smt2 b/test/regress/regress0/arith/arith-tighten-1.smt2
index 237d5b144..a8a5234a0 100644
--- a/test/regress/regress0/arith/arith-tighten-1.smt2
+++ b/test/regress/regress0/arith/arith-tighten-1.smt2
@@ -1,17 +1,19 @@
-; COMMAND-LINE: --no-check-unsat-cores --no-check-proofs
+; COMMAND-LINE: --no-check-unsat-cores
 ; EXPECT: unsat
 (set-logic QF_LIRA)
 
-(declare-fun n () Int)
+(declare-fun i () Int)
+(declare-fun j () Int)
+(declare-fun x () Real)
+(declare-fun y () Real)
 
-; tests tightenings of the form [Int] >= r   to [Int] >= ceiling(r)
-; where r is a real.
-(assert
-    (and
-        (>= n 1.5)
-        (<= n 1.9)
-    )
-)
+
+
+(assert (= x y))
+(assert (= x (- 2.5 y)))
+(assert (>= (+ i j) x))
+(assert (<= j (+ x 0.5)))
+(assert (<= i 0))
 
 (check-sat)
 
diff --git a/test/regress/regress0/arith/arith-tighten-2.smt2 b/test/regress/regress0/arith/arith-tighten-2.smt2
new file mode 100644
index 000000000..24eec2977
--- /dev/null
+++ b/test/regress/regress0/arith/arith-tighten-2.smt2
@@ -0,0 +1,12 @@
+; COMMAND-LINE: --no-check-unsat-cores
+; EXPECT: unsat
+(set-logic QF_LIA)
+
+(declare-fun i () Int)
+(declare-fun j () Int)
+
+(assert (> (+ i j) 1))
+(assert (< i 1))
+(assert (< j 1))
+
+(check-sat)
diff --git a/test/regress/regress0/arith/bug569.smt2 b/test/regress/regress0/arith/bug569.smt2
index 1a63f265b..e1ca49ac5 100644
--- a/test/regress/regress0/arith/bug569.smt2
+++ b/test/regress/regress0/arith/bug569.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --no-check-unsat-cores --no-check-proofs
+; COMMAND-LINE: --no-check-unsat-cores
 ; EXPECT: unsat
 (set-logic QF_AUFLIRA)
 (set-info :smt-lib-version 2.0)
diff --git a/test/regress/regress0/arith/integers/ackermann4.smt2 b/test/regress/regress0/arith/integers/ackermann4.smt2
index 1b76e1075..34aa56480 100644
--- a/test/regress/regress0/arith/integers/ackermann4.smt2
+++ b/test/regress/regress0/arith/integers/ackermann4.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --ackermann --no-check-models --no-check-proofs --no-check-unsat-cores
+; COMMAND-LINE: --ackermann --no-check-models --no-check-unsat-cores
 ; EXPECT: unsat
 (set-logic QF_ALIA)
 (set-info :smt-lib-version 2.0)
diff --git a/test/regress/regress0/arith/integers/ackermann5.smt2 b/test/regress/regress0/arith/integers/ackermann5.smt2
index 8b93a3c35..debd29344 100644
--- a/test/regress/regress0/arith/integers/ackermann5.smt2
+++ b/test/regress/regress0/arith/integers/ackermann5.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --ackermann --no-check-models --no-check-proofs --no-check-unsat-cores
+; COMMAND-LINE: --ackermann --no-check-models
 ; EXPECT: sat
 (set-logic QF_UFLIA)
 (set-info :smt-lib-version 2.0)
diff --git a/test/regress/regress0/arith/integers/ackermann6.smt2 b/test/regress/regress0/arith/integers/ackermann6.smt2
index 62f2f1276..78f5a3658 100644
--- a/test/regress/regress0/arith/integers/ackermann6.smt2
+++ b/test/regress/regress0/arith/integers/ackermann6.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --ackermann --no-check-models --no-check-proofs --no-check-unsat-cores
+; COMMAND-LINE: --ackermann --no-check-models --no-check-unsat-cores
 ; EXPECT: unsat
 (set-logic QF_UFLIA)
 (set-info :smt-lib-version 2.0)
diff --git a/test/regress/regress0/lemmas/sc_init_frame_gap.induction.smtv1.smt2 b/test/regress/regress0/lemmas/sc_init_frame_gap.induction.smtv1.smt2
index 26796d27b..8101dfdeb 100644
--- a/test/regress/regress0/lemmas/sc_init_frame_gap.induction.smtv1.smt2
+++ b/test/regress/regress0/lemmas/sc_init_frame_gap.induction.smtv1.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --no-check-proofs
+; COMMAND-LINE:
 (set-option :incremental false)
 (set-info :source "The Formal Verification of a Reintegration Protocol. Author: Lee Pike. Website: http://www.cs.indiana.edu/~lepike/pub_pages/emsoft.html.
 
diff --git a/test/regress/regress1/lemmas/pursuit-safety-8.smtv1.smt2 b/test/regress/regress1/lemmas/pursuit-safety-8.smtv1.smt2
index 14000f941..6187be7c1 100644
--- a/test/regress/regress1/lemmas/pursuit-safety-8.smtv1.smt2
+++ b/test/regress/regress1/lemmas/pursuit-safety-8.smtv1.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --no-check-proofs
+; COMMAND-LINE:
 (set-option :incremental false)
 (set-info :source "SAL benchmark suite.  Created at SRI by Bruno Dutertre, John Rushby, Maria
 Sorea, and Leonardo de Moura.  Contact demoura@csl.sri.com for more
diff --git a/test/regress/regress1/lemmas/simple_startup_9nodes.abstract.base.smtv1.smt2 b/test/regress/regress1/lemmas/simple_startup_9nodes.abstract.base.smtv1.smt2
index 3e10f6aab..4aa162f5b 100644
--- a/test/regress/regress1/lemmas/simple_startup_9nodes.abstract.base.smtv1.smt2
+++ b/test/regress/regress1/lemmas/simple_startup_9nodes.abstract.base.smtv1.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --no-check-proofs
+; COMMAND-LINE:
 (set-option :incremental false)
 (set-info :source "TTA Startup. Bruno Dutertre (bruno@csl.sri.com)")
 (set-info :status unsat)