Merge branch 'master' into fixBetterSkolems

47 files changed, 667 insertions, 264 deletions

diff --git a/contrib/run-script-smtcomp2019 b/contrib/run-script-smtcomp2019
index d25783453..a8c6b0ba4 100755
--- a/contrib/run-script-smtcomp2019
+++ b/contrib/run-script-smtcomp2019
@@ -27,7 +27,7 @@ function finishwith {
 case "$logic" in
 
 QF_LRA)
-  trywith 200 --miplib-trick --miplib-trick-subs=4 --use-approx --lemmas-on-replay-failure --replay-early-close-depth=4 --replay-lemma-reject-cut=128 --replay-reject-cut=512 --unconstrained-simp --use-soi
+  trywith 400 --miplib-trick --miplib-trick-subs=4 --use-approx --lemmas-on-replay-failure --replay-early-close-depth=4 --replay-lemma-reject-cut=128 --replay-reject-cut=512 --unconstrained-simp --use-soi
   finishwith --no-restrict-pivots --use-soi --new-prop --unconstrained-simp
   ;;
 QF_LIA)
@@ -35,94 +35,97 @@ QF_LIA)
   finishwith --miplib-trick --miplib-trick-subs=4 --use-approx --lemmas-on-replay-failure --replay-early-close-depth=4 --replay-lemma-reject-cut=128 --replay-reject-cut=512 --unconstrained-simp --use-soi --pb-rewrites
   ;;
 QF_NIA)
-  trywith 300 --nl-ext-tplanes --decision=internal
-  trywith 30 --nl-ext-tplanes --decision=justification
-  trywith 30 --no-nl-ext-tplanes --decision=internal
-  # this totals up to more than 20 minutes, although notice that smaller bit-widths may quickly fail
-  trywith 300 --solve-int-as-bv=2 --bitblast=eager --bv-sat-solver=cadical --bitblast-aig --no-bv-abstraction
-  trywith 300 --solve-int-as-bv=4 --bitblast=eager --bv-sat-solver=cadical --bitblast-aig --no-bv-abstraction
-  trywith 300 --solve-int-as-bv=8 --bitblast=eager --bv-sat-solver=cadical --bitblast-aig --no-bv-abstraction
-  trywith 300 --solve-int-as-bv=16 --bitblast=eager --bv-sat-solver=cadical --bitblast-aig --no-bv-abstraction
-  trywith 600 --solve-int-as-bv=32 --bitblast=eager --bv-sat-solver=cadical --bitblast-aig --no-bv-abstraction
+  trywith 600 --nl-ext-tplanes --decision=internal
+  trywith 60 --nl-ext-tplanes --decision=justification
+  trywith 60 --no-nl-ext-tplanes --decision=internal
+  # this totals up to more than 40 minutes, although notice that smaller bit-widths may quickly fail
+  trywith 600 --solve-int-as-bv=2 --bitblast=eager --bv-sat-solver=cadical --no-bv-abstraction
+  trywith 600 --solve-int-as-bv=4 --bitblast=eager --bv-sat-solver=cadical --no-bv-abstraction
+  trywith 600 --solve-int-as-bv=8 --bitblast=eager --bv-sat-solver=cadical --no-bv-abstraction
+  trywith 600 --solve-int-as-bv=16 --bitblast=eager --bv-sat-solver=cadical --no-bv-abstraction
+  trywith 1200 --solve-int-as-bv=32 --bitblast=eager --bv-sat-solver=cadical --no-bv-abstraction
   finishwith --nl-ext-tplanes --decision=internal
   ;;
 QF_NRA)
-  trywith 300 --nl-ext-tplanes --decision=internal
-  trywith 300 --nl-ext-tplanes --decision=justification --no-nl-ext-factor
-  trywith 30 --nl-ext-tplanes --decision=internal --solve-real-as-int
+  trywith 600 --nl-ext-tplanes --decision=internal
+  trywith 600 --nl-ext-tplanes --decision=justification --no-nl-ext-factor
+  trywith 60 --nl-ext-tplanes --decision=internal --solve-real-as-int
   finishwith --nl-ext-tplanes --decision=justification
   ;;
 # all logics with UF + quantifiers should either fall under this or special cases below
 ALIA|AUFLIA|AUFLIRA|AUFNIRA|UF|UFIDL|UFLIA|UFLRA|UFNIA|UFDT|UFDTLIA|AUFDTLIA|AUFBVDTLIA|AUFNIA)
   # the following is designed for a run time of 20 min.
-  # initial runs 1min
-  trywith 30 --simplification=none --full-saturate-quant
-  trywith 30 --no-e-matching --full-saturate-quant
-  # trigger selections 3min
-  trywith 30 --relevant-triggers --full-saturate-quant
-  trywith 30 --trigger-sel=max --full-saturate-quant
-  trywith 30 --multi-trigger-when-single --full-saturate-quant
-  trywith 30 --multi-trigger-when-single --multi-trigger-priority --full-saturate-quant
-  trywith 30 --multi-trigger-cache --full-saturate-quant
-  trywith 30 --no-multi-trigger-linear --full-saturate-quant
-  # other 4min
-  trywith 30 --pre-skolem-quant --full-saturate-quant
-  trywith 30 --inst-when=full --full-saturate-quant
-  trywith 30 --no-e-matching --no-quant-cf --full-saturate-quant
-  trywith 30 --full-saturate-quant --quant-ind
-  trywith 30 --decision=internal --simplification=none --no-inst-no-entail --no-quant-cf --full-saturate-quant
-  trywith 30 --decision=internal --full-saturate-quant
-  trywith 30 --term-db-mode=relevant --full-saturate-quant
-  trywith 30 --fs-interleave --full-saturate-quant
-  # finite model find 3min
-  trywith 30 --finite-model-find --mbqi=none
-  trywith 30 --finite-model-find --decision=internal
-  trywith 30 --finite-model-find --macros-quant --macros-quant-mode=all
-  trywith 30 --finite-model-find --uf-ss=no-minimal
-  trywith 60 --finite-model-find --fmf-inst-engine
-  # long runs 9min
-  trywith 240 --finite-model-find --decision=internal
+  # initial runs 2min
+  trywith 60 --simplification=none --full-saturate-quant
+  trywith 60 --no-e-matching --full-saturate-quant
+  # trigger selections 6min
+  trywith 60 --relevant-triggers --full-saturate-quant
+  trywith 60 --trigger-sel=max --full-saturate-quant
+  trywith 60 --multi-trigger-when-single --full-saturate-quant
+  trywith 60 --multi-trigger-when-single --multi-trigger-priority --full-saturate-quant
+  trywith 60 --multi-trigger-cache --full-saturate-quant
+  trywith 60 --no-multi-trigger-linear --full-saturate-quant
+  # other 8min
+  trywith 60 --pre-skolem-quant --full-saturate-quant
+  trywith 60 --inst-when=full --full-saturate-quant
+  trywith 60 --no-e-matching --no-quant-cf --full-saturate-quant
+  trywith 60 --full-saturate-quant --quant-ind
+  trywith 60 --decision=internal --simplification=none --no-inst-no-entail --no-quant-cf --full-saturate-quant
+  trywith 60 --decision=internal --full-saturate-quant
+  trywith 60 --term-db-mode=relevant --full-saturate-quant
+  trywith 60 --fs-interleave --full-saturate-quant
+  # finite model find 6min
+  trywith 60 --finite-model-find --mbqi=none
+  trywith 60 --finite-model-find --decision=internal
+  trywith 60 --finite-model-find --macros-quant --macros-quant-mode=all
+  trywith 60 --finite-model-find --uf-ss=no-minimal
+  trywith 120 --finite-model-find --fmf-inst-engine
+  # long runs 8min
+  trywith 480 --finite-model-find --decision=internal
   finishwith --full-saturate-quant
   ;;
 ABVFP|BVFP|FP)
-  finishwith --full-saturate-quant
+  finishwith --full-saturate-quant --fp-exp
   ;;
 UFBV)
   # most problems in UFBV are essentially BV
-  trywith 300 --full-saturate-quant --decision=internal
-  trywith 300 --full-saturate-quant --cbqi-nested-qe --decision=internal
-  trywith 30 --full-saturate-quant --no-cbqi-innermost --global-negate
+  trywith 600 --full-saturate-quant --decision=internal
+  trywith 600 --full-saturate-quant --cbqi-nested-qe --decision=internal
+  trywith 60 --full-saturate-quant --no-cbqi-innermost --global-negate
   finishwith --finite-model-find
   ;;
 BV)
-  trywith 120 --full-saturate-quant
-  trywith 120 --full-saturate-quant --no-cbqi-innermost
-  trywith 300 --full-saturate-quant --cbqi-nested-qe --decision=internal
-  trywith 30 --full-saturate-quant --no-cbqi-bv
-  trywith 30 --full-saturate-quant --cbqi-bv-ineq=eq-slack
+  trywith 240 --full-saturate-quant
+  trywith 240 --full-saturate-quant --no-cbqi-innermost
+  trywith 600 --full-saturate-quant --cbqi-nested-qe --decision=internal
+  trywith 60 --full-saturate-quant --no-cbqi-bv
+  trywith 60 --full-saturate-quant --cbqi-bv-ineq=eq-slack
   # finish 10min
   finishwith --full-saturate-quant --no-cbqi-innermost --global-negate
   ;;
 LIA|LRA|NIA|NRA)
-  trywith 30 --full-saturate-quant --nl-ext-tplanes
-  trywith 300 --full-saturate-quant --no-cbqi-innermost
-  trywith 300 --full-saturate-quant --cbqi-nested-qe
+  trywith 60 --full-saturate-quant --nl-ext-tplanes
+  trywith 600 --full-saturate-quant --no-cbqi-innermost
+  trywith 600 --full-saturate-quant --cbqi-nested-qe
   finishwith --full-saturate-quant --cbqi-nested-qe --decision=internal
   ;;
 QF_AUFBV)
-  trywith 600
+  trywith 1200
   finishwith --decision=justification-stoponly
   ;;
 QF_ABV)
-  trywith 50 --ite-simp --simp-with-care --repeat-simp --arrays-weak-equiv
-  trywith 500 --arrays-weak-equiv
+  trywith 100 --ite-simp --simp-with-care --repeat-simp --arrays-weak-equiv
+  trywith 1000 --arrays-weak-equiv
   finishwith --ite-simp --simp-with-care --repeat-simp --arrays-weak-equiv
   ;;
 QF_UFBV)
-  finishwith --bitblast=eager --bv-sat-solver=cadical
+  # Benchmarks with uninterpreted sorts cannot be solved with eager
+  # bit-blasting currently
+  trywith 2400 --bitblast=eager --bv-sat-solver=cadical
+  finishwith
   ;;
 QF_BV)
-  finishwith --unconstrained-simp --bv-div-zero-const --bv-intro-pow2 --bitblast=eager --bv-sat-solver=cadical --bitblast-aig --bv-eq-slicer=auto --no-bv-abstraction
+  finishwith --bv-div-zero-const --bitblast=eager --bv-sat-solver=cadical --no-bv-abstraction
   ;;
 QF_AUFLIA)
   finishwith --no-arrays-eager-index --arrays-eager-lemmas --decision=justification
@@ -134,7 +137,7 @@ QF_AUFNIA)
   finishwith --decision=justification --no-arrays-eager-index --arrays-eager-lemmas
   ;;
 QF_ALIA)
-  trywith 70 --decision=justification --arrays-weak-equiv
+  trywith 140 --decision=justification --arrays-weak-equiv
   finishwith --decision=justification-stoponly --no-arrays-eager-index --arrays-eager-lemmas
   ;;
 QF_S|QF_SLIA)
@@ -142,13 +145,13 @@ QF_S|QF_SLIA)
   finishwith --strings-exp --rewrite-divk --lang=smt2.6.1
   ;;
 QF_ABVFP)
-  finishwith
+  finishwith --fp-exp
   ;;
 QF_BVFP)
-  finishwith
+  finishwith --fp-exp
   ;;
 QF_FP)
-  finishwith
+  finishwith --fp-exp
   ;;
 *)
   # just run the default
diff --git a/contrib/run-script-smtcomp2019-model-validation b/contrib/run-script-smtcomp2019-model-validation
index f4b812fd6..eec17294d 100755
--- a/contrib/run-script-smtcomp2019-model-validation
+++ b/contrib/run-script-smtcomp2019-model-validation
@@ -14,7 +14,7 @@ function finishwith {
 case "$logic" in
 
 QF_BV)
-  finishwith --bv-div-zero-const --bv-intro-pow2 --bitblast=eager --bv-sat-solver=cadical --bv-eq-slicer=auto --no-bv-abstraction
+  finishwith --bv-div-zero-const --bitblast=eager --bv-sat-solver=cadical --no-bv-abstraction
   ;;
 *)
   # just run the default
diff --git a/contrib/run-script-smtcomp2019-unsat-cores b/contrib/run-script-smtcomp2019-unsat-cores
index 1454e7a8a..795de734b 100755
--- a/contrib/run-script-smtcomp2019-unsat-cores
+++ b/contrib/run-script-smtcomp2019-unsat-cores
@@ -14,10 +14,10 @@ function finishwith {
 case "$logic" in
 
 QF_LRA)
-  finishwith --no-restrict-pivots --use-soi --new-prop --unconstrained-simp
+  finishwith --no-restrict-pivots --use-soi --new-prop
   ;;
 QF_LIA)
-  finishwith --miplib-trick --miplib-trick-subs=4 --use-approx --lemmas-on-replay-failure --replay-early-close-depth=4 --replay-lemma-reject-cut=128 --replay-reject-cut=512 --unconstrained-simp --use-soi
+  finishwith --miplib-trick --miplib-trick-subs=4 --use-approx --lemmas-on-replay-failure --replay-early-close-depth=4 --replay-lemma-reject-cut=128 --replay-reject-cut=512 --use-soi
   ;;
 QF_NIA)
   finishwith --solve-int-as-bv=32 --bitblast=eager --bv-sat-solver=cryptominisat
@@ -27,7 +27,7 @@ QF_NRA)
   ;;
 # all logics with UF + quantifiers should either fall under this or special cases below
 ALIA|AUFLIA|AUFLIRA|AUFNIRA|UF|UFIDL|UFLIA|UFLRA|UFNIA|UFDT|UFDTLIA|AUFDTLIA|AUFBVDTLIA|AUFNIA|ABVFP|BVFP|FP)
-  finishwith --full-saturate-quant
+  finishwith --full-saturate-quant --fp-exp
   ;;
 UFBV)
   finishwith --finite-model-find
@@ -48,7 +48,7 @@ QF_ABV)
   finishwith --ite-simp --simp-with-care --arrays-weak-equiv
   ;;
 QF_UFBV)
-  finishwith --bitblast=eager --bv-sat-solver=cryptominisat
+  finishwith
   ;;
 QF_BV)
   finishwith --bv-div-zero-const --bv-eq-slicer=auto --no-bv-abstraction
@@ -65,14 +65,17 @@ QF_AUFNIA)
 QF_ALIA)
   finishwith --decision=justification-stoponly --no-arrays-eager-index --arrays-eager-lemmas
   ;;
+QF_S|QF_SLIA)
+  finishwith --strings-exp --rewrite-divk --lang=smt2.6.1
+  ;;
 QF_ABVFP)
-  finishwith
+  finishwith --fp-exp
   ;;
 QF_BVFP)
-  finishwith
+  finishwith --fp-exp
   ;;
 QF_FP)
-  finishwith
+  finishwith --fp-exp
   ;;
 *)
   # just run the default
diff --git a/proofs/signatures/CMakeLists.txt b/proofs/signatures/CMakeLists.txt
index 6e9c8947d..86474585c 100644
--- a/proofs/signatures/CMakeLists.txt
+++ b/proofs/signatures/CMakeLists.txt
@@ -16,6 +16,7 @@ set(core_signature_files
     th_bv_rewrites.plf
     th_real.plf
     th_int.plf
+    th_lra.plf
 )
 
 set(CORE_SIGNATURES "")
diff --git a/proofs/signatures/drat.plf b/proofs/signatures/drat.plf
index d0f647452..fa7ca3055 100644
--- a/proofs/signatures/drat.plf
+++ b/proofs/signatures/drat.plf
@@ -113,9 +113,10 @@
                                       ((clc l c') (cnf_has_bottom rest))))))
 
 ; Return a new cnf with one copy of this clause removed.
+; If the clause is absent, returns the original cnf.
 (program cnf_remove_clause ((c clause) (cs cnf)) cnf
          (match cs
-                (cnfn (fail cnf))
+                (cnfn cnfn)
                 ((cnfc c' cs')
                  (match (clause_eq c c')
                         (tt cs')
@@ -224,9 +225,11 @@
                 (tt tt)
                 (ff (match (is_at cs c)
                            (tt tt)
-                           (ff (are_all_at
+                           (ff (match c
+                                      (cln ff)
+                                      ((clc a b) (are_all_at ; dedent
                                  cs
-                                 (collect_pseudo_resolvents cs c)))))))
+                                 (collect_pseudo_resolvents cs c)))))))))
 
 ; Is this proof a valid DRAT proof of bottom?
 (program is_specified_drat_proof ((f cnf) (proof DRATProof)) bool
diff --git a/proofs/signatures/lrat.plf b/proofs/signatures/lrat.plf
index ea1d90537..d16791624 100644
--- a/proofs/signatures/lrat.plf
+++ b/proofs/signatures/lrat.plf
@@ -361,14 +361,14 @@
 ; unit, it modifies the global assignment to satisfy the clause, and returns
 ; the literal that was made SAT by the new mark.
 ;
-; Fails if `c` is a TAUT
+; If `c` is a tautology, reports `MRSat`, since it is (trivially) satisfied.
 (program clause_check_unit_and_maybe_mark ((c clause)) MarkResult
          (match (clause_is_sat c)
                 (tt MRSat)
                 (ff (match (clause_is_unsat c)
                            (tt MRUnsat)
                            (ff (match (is_t c)
-                                      (tt (fail MarkResult))
+                                      (tt MRSat)
                                       (ff ; Dedent
          (match (clause_has_floating c)
                 (tt (let first (clause_first_floating c)
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index cff31dbcd..011ba6ab5 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -137,8 +137,8 @@ libcvc4_add_sources(
   proof/clause_id.h
   proof/cnf_proof.cpp
   proof/cnf_proof.h
-  proof/dimacs_printer.cpp
-  proof/dimacs_printer.h
+  proof/dimacs.cpp
+  proof/dimacs.h
   proof/drat/drat_proof.cpp
   proof/drat/drat_proof.h
   proof/er/er_proof.cpp
diff --git a/src/bindings/java/CMakeLists.txt b/src/bindings/java/CMakeLists.txt
index 7b7d93f1d..b1631f369 100644
--- a/src/bindings/java/CMakeLists.txt
+++ b/src/bindings/java/CMakeLists.txt
@@ -131,6 +131,7 @@ set(gen_java_files
   ${CMAKE_CURRENT_BINARY_DIR}/LastExceptionBuffer.java
   ${CMAKE_CURRENT_BINARY_DIR}/LogicException.java
   ${CMAKE_CURRENT_BINARY_DIR}/LogicInfo.java
+  ${CMAKE_CURRENT_BINARY_DIR}/Map_ExprExpr.java
   ${CMAKE_CURRENT_BINARY_DIR}/ModalException.java
   ${CMAKE_CURRENT_BINARY_DIR}/OptionException.java
   ${CMAKE_CURRENT_BINARY_DIR}/Options.java
@@ -165,7 +166,6 @@ set(gen_java_files
   ${CMAKE_CURRENT_BINARY_DIR}/SExpr.java
   ${CMAKE_CURRENT_BINARY_DIR}/SExprKeyword.java
   ${CMAKE_CURRENT_BINARY_DIR}/SExprType.java
-  ${CMAKE_CURRENT_BINARY_DIR}/Statistic.java
   ${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_CVC4__Model.java
   ${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_CVC4__Printer.java
   ${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_CVC4__api__Solver.java
@@ -178,7 +178,6 @@ set(gen_java_files
   ${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_mpq_class.java
   ${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_mpz_class.java
   ${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_std__istream.java
-  ${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_std__mapT_CVC4__Expr_CVC4__Expr_t.java
   ${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_std__ostream.java
   ${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_std__shared_ptrT_CVC4__SygusPrintCallback_t.java
   ${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_std__string.java
@@ -201,16 +200,17 @@ set(gen_java_files
   ${CMAKE_CURRENT_BINARY_DIR}/SmtEngine.java
   ${CMAKE_CURRENT_BINARY_DIR}/SortConstructorType.java
   ${CMAKE_CURRENT_BINARY_DIR}/SortType.java
+  ${CMAKE_CURRENT_BINARY_DIR}/Statistic.java
   ${CMAKE_CURRENT_BINARY_DIR}/Statistics.java
   ${CMAKE_CURRENT_BINARY_DIR}/StatisticsBase.java
   ${CMAKE_CURRENT_BINARY_DIR}/StringType.java
   ${CMAKE_CURRENT_BINARY_DIR}/SygusConstraintCommand.java
-  ${CMAKE_CURRENT_BINARY_DIR}/SynthFunCommand.java
   ${CMAKE_CURRENT_BINARY_DIR}/SygusGTerm.java
   ${CMAKE_CURRENT_BINARY_DIR}/SygusInvConstraintCommand.java
   ${CMAKE_CURRENT_BINARY_DIR}/SygusPrintCallback.java
   ${CMAKE_CURRENT_BINARY_DIR}/SymbolTable.java
   ${CMAKE_CURRENT_BINARY_DIR}/SymbolType.java
+  ${CMAKE_CURRENT_BINARY_DIR}/SynthFunCommand.java
   ${CMAKE_CURRENT_BINARY_DIR}/TesterType.java
   ${CMAKE_CURRENT_BINARY_DIR}/TheoryId.java
   ${CMAKE_CURRENT_BINARY_DIR}/Timer.java
diff --git a/src/expr/node_algorithm.cpp b/src/expr/node_algorithm.cpp
index 25ffb0778..841f9ea28 100644
--- a/src/expr/node_algorithm.cpp
+++ b/src/expr/node_algorithm.cpp
@@ -236,6 +236,38 @@ bool getFreeVariables(TNode n,
   return !fvs.empty();
 }
 
+bool getVariables(TNode n, std::unordered_set<TNode, TNodeHashFunction>& vs)
+{
+  std::unordered_set<TNode, TNodeHashFunction> visited;
+  std::vector<TNode> visit;
+  TNode cur;
+  visit.push_back(n);
+  do
+  {
+    cur = visit.back();
+    visit.pop_back();
+    std::unordered_set<TNode, TNodeHashFunction>::iterator itv =
+        visited.find(cur);
+    if (itv == visited.end())
+    {
+      if (cur.isVar())
+      {
+        vs.insert(cur);
+      }
+      else
+      {
+        for (const TNode& cn : cur)
+        {
+          visit.push_back(cn);
+        }
+      }
+      visited.insert(cur);
+    }
+  } while (!visit.empty());
+
+  return !vs.empty();
+}
+
 void getSymbols(TNode n, std::unordered_set<Node, NodeHashFunction>& syms)
 {
   std::unordered_set<TNode, TNodeHashFunction> visited;
diff --git a/src/expr/node_algorithm.h b/src/expr/node_algorithm.h
index 656f162ae..727f5ba75 100644
--- a/src/expr/node_algorithm.h
+++ b/src/expr/node_algorithm.h
@@ -73,6 +73,14 @@ bool getFreeVariables(TNode n,
                       bool computeFv = true);
 
 /**
+ * Get all variables in n.
+ * @param n The node under investigation
+ * @param vs The set which free variables are added to
+ * @return true iff this node contains a free variable.
+ */
+bool getVariables(TNode n, std::unordered_set<TNode, TNodeHashFunction>& vs);
+
+/**
  * For term n, this function collects the symbols that occur as a subterms
  * of n. A symbol is a variable that does not have kind BOUND_VARIABLE.
  * @param n The node under investigation
diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h
index 9128bc190..4558f3720 100644
--- a/src/expr/node_builder.h
+++ b/src/expr/node_builder.h
@@ -772,8 +772,8 @@ void NodeBuilder<nchild_thresh>::clear(Kind k) {
 
 template <unsigned nchild_thresh>
 void NodeBuilder<nchild_thresh>::realloc(size_t toSize) {
-  Assert( toSize > d_nvMaxChildren,
-          "attempt to realloc() a NodeBuilder to a smaller/equal size!" );
+  AlwaysAssert(toSize > d_nvMaxChildren,
+               "attempt to realloc() a NodeBuilder to a smaller/equal size!");
   Assert( toSize < (1lu << CVC4__EXPR__NODE_VALUE__NBITS__NCHILDREN),
           "attempt to realloc() a NodeBuilder to size %u (beyond hard limit of %u)",
           toSize, (1lu << CVC4__EXPR__NODE_VALUE__NBITS__NCHILDREN) - 1 );
diff --git a/src/printer/dagification_visitor.cpp b/src/printer/dagification_visitor.cpp
index cf5f35457..a024c97a7 100644
--- a/src/printer/dagification_visitor.cpp
+++ b/src/printer/dagification_visitor.cpp
@@ -17,6 +17,8 @@
 #include "printer/dagification_visitor.h"
 
 #include "context/context.h"
+#include "expr/node_algorithm.h"
+#include "expr/node_manager_attributes.h"
 #include "theory/substitutions.h"
 
 #include <sstream>
@@ -24,18 +26,20 @@
 namespace CVC4 {
 namespace printer {
 
-DagificationVisitor::DagificationVisitor(unsigned threshold, std::string letVarPrefix) :
-  d_threshold(threshold),
-  d_letVarPrefix(letVarPrefix),
-  d_nodeCount(),
-  d_top(),
-  d_context(new context::Context()),
-  d_substitutions(new theory::SubstitutionMap(d_context)),
-  d_letVar(0),
-  d_done(false),
-  d_uniqueParent(),
-  d_substNodes() {
-
+DagificationVisitor::DagificationVisitor(unsigned threshold,
+                                         std::string letVarPrefix)
+    : d_threshold(threshold),
+      d_letVarPrefix(letVarPrefix),
+      d_nodeCount(),
+      d_reservedLetNames(),
+      d_top(),
+      d_context(new context::Context()),
+      d_substitutions(new theory::SubstitutionMap(d_context)),
+      d_letVar(0),
+      d_done(false),
+      d_uniqueParent(),
+      d_substNodes()
+{
   // 0 doesn't make sense
   AlwaysAssertArgument(threshold > 0, threshold);
 }
@@ -51,8 +55,28 @@ bool DagificationVisitor::alreadyVisited(TNode current, TNode parent) {
   {
     // for quantifiers, we visit them but we don't recurse on them
     visit(current, parent);
+
+    // search for variables that start with the let prefix
+    std::unordered_set<TNode, TNodeHashFunction> vs;
+    expr::getVariables(current, vs);
+    for (const TNode v : vs)
+    {
+      const std::string name = v.getAttribute(expr::VarNameAttr());
+      if (name.compare(0, d_letVarPrefix.size(), d_letVarPrefix) == 0)
+      {
+        d_reservedLetNames.insert(name);
+      }
+    }
     return true;
   }
+  else if (current.isVar())
+  {
+    const std::string name = current.getAttribute(expr::VarNameAttr());
+    if (name.compare(0, d_letVarPrefix.size(), d_letVarPrefix) == 0)
+    {
+      d_reservedLetNames.insert(name);
+    }
+  }
   // don't visit variables, constants, or those exprs that we've
   // already seen more than the threshold: if we've increased
   // the count beyond the threshold already, we've done the same
@@ -137,7 +161,11 @@ void DagificationVisitor::done(TNode node) {
 
     // construct the let binder
     std::stringstream ss;
-    ss << d_letVarPrefix << d_letVar++;
+    do
+    {
+      ss.str("");
+      ss << d_letVarPrefix << d_letVar++;
+    } while (d_reservedLetNames.find(ss.str()) != d_reservedLetNames.end());
     Node letvar = NodeManager::currentNM()->mkSkolem(ss.str(), (*i).getType(), "dagification", NodeManager::SKOLEM_NO_NOTIFY | NodeManager::SKOLEM_EXACT_NAME);
 
     // apply previous substitutions to the rhs, enabling cascading LETs
diff --git a/src/printer/dagification_visitor.h b/src/printer/dagification_visitor.h
index 18f31e662..6df5f32b4 100644
--- a/src/printer/dagification_visitor.h
+++ b/src/printer/dagification_visitor.h
@@ -21,6 +21,7 @@
 
 #include <string>
 #include <unordered_map>
+#include <unordered_set>
 #include <vector>
 
 #include "expr/node.h"
@@ -69,6 +70,12 @@ class DagificationVisitor {
   std::unordered_map<TNode, unsigned, TNodeHashFunction> d_nodeCount;
 
   /**
+   * The set of variable names with the let prefix that appear in the
+   * expression.
+   */
+  std::unordered_set<std::string> d_reservedLetNames;
+
+  /**
    * The top-most node we are visiting.
    */
   TNode d_top;
diff --git a/src/proof/clausal_bitvector_proof.cpp b/src/proof/clausal_bitvector_proof.cpp
index eed295b1a..07589fd07 100644
--- a/src/proof/clausal_bitvector_proof.cpp
+++ b/src/proof/clausal_bitvector_proof.cpp
@@ -17,24 +17,35 @@
 #include "cvc4_private.h"
 
 #include <algorithm>
+#include <iostream>
 #include <iterator>
-#include <set>
+#include <unordered_set>
 
 #include "options/bv_options.h"
 #include "proof/clausal_bitvector_proof.h"
+#include "proof/dimacs.h"
 #include "proof/drat/drat_proof.h"
 #include "proof/er/er_proof.h"
 #include "proof/lfsc_proof_printer.h"
 #include "proof/lrat/lrat_proof.h"
 #include "theory/bv/theory_bv.h"
 
+#if CVC4_USE_DRAT2ER
+#include "drat2er_options.h"
+#include "drat_trim_interface.h"
+#endif
+
 namespace CVC4 {
 
 namespace proof {
 
 ClausalBitVectorProof::ClausalBitVectorProof(theory::bv::TheoryBV* bv,
                                              TheoryProofEngine* proofEngine)
-    : BitVectorProof(bv, proofEngine), d_usedClauses(), d_binaryDratProof()
+    : BitVectorProof(bv, proofEngine),
+      d_clauses(),
+      d_originalClauseIndices(),
+      d_binaryDratProof(),
+      d_coreClauseIndices()
 {
 }
 
@@ -69,33 +80,151 @@ void ClausalBitVectorProof::initCnfProof(prop::CnfStream* cnfStream,
 void ClausalBitVectorProof::registerUsedClause(ClauseId id,
                                                prop::SatClause& clause)
 {
-  d_usedClauses.emplace_back(id, clause);
+  d_clauses.emplace(id, clause);
+  d_originalClauseIndices.push_back(id);
 };
 
 void ClausalBitVectorProof::calculateAtomsInBitblastingProof()
 {
+  optimizeDratProof();
+
   // Debug dump of DRAT Proof
   if (Debug.isOn("bv::clausal"))
   {
     std::string serializedDratProof = d_binaryDratProof.str();
+    Debug("bv::clausal") << "option: " << options::bvOptimizeSatProof()
+                         << std::endl;
     Debug("bv::clausal") << "binary DRAT proof byte count: "
                          << serializedDratProof.size() << std::endl;
-    Debug("bv::clausal") << "Parsing DRAT proof ... " << std::endl;
-    drat::DratProof dratProof =
-        drat::DratProof::fromBinary(serializedDratProof);
-
-    Debug("bv::clausal") << "Printing DRAT proof ... " << std::endl;
-    dratProof.outputAsText(Debug("bv::clausal"));
+    Debug("bv::clausal") << "clause count: " << d_coreClauseIndices.size()
+                         << std::endl;
   }
 
   // Empty any old record of which atoms were used
   d_atomsInBitblastingProof.clear();
+  Assert(d_atomsInBitblastingProof.size() == 0);
 
   // For each used clause, ask the CNF proof which atoms are used in it
-  for (const auto& usedIndexAndClause : d_usedClauses)
+  for (const ClauseId usedIdx : d_coreClauseIndices)
   {
-    d_cnfProof->collectAtoms(&usedIndexAndClause.second,
-                             d_atomsInBitblastingProof);
+    d_cnfProof->collectAtoms(&d_clauses.at(usedIdx), d_atomsInBitblastingProof);
+  }
+}
+
+void ClausalBitVectorProof::optimizeDratProof()
+{
+  if (options::bvOptimizeSatProof()
+          == theory::bv::BvOptimizeSatProof::BITVECTOR_OPTIMIZE_SAT_PROOF_PROOF
+      || options::bvOptimizeSatProof()
+             == theory::bv::BvOptimizeSatProof::
+                    BITVECTOR_OPTIMIZE_SAT_PROOF_FORMULA)
+  {
+    Debug("bv::clausal") << "Optimizing DRAT" << std::endl;
+    char formulaFilename[] = "/tmp/cvc4-dimacs-XXXXXX";
+    char dratFilename[] = "/tmp/cvc4-drat-XXXXXX";
+    char optDratFilename[] = "/tmp/cvc4-optimized-drat-XXXXXX";
+    char optFormulaFilename[] = "/tmp/cvc4-optimized-formula-XXXXXX";
+    int r;
+    r = mkstemp(formulaFilename);
+    AlwaysAssert(r > 0);
+    close(r);
+    r = mkstemp(dratFilename);
+    AlwaysAssert(r > 0);
+    close(r);
+    r = mkstemp(optDratFilename);
+    AlwaysAssert(r > 0);
+    close(r);
+    r = mkstemp(optFormulaFilename);
+    AlwaysAssert(r > 0);
+    close(r);
+
+    std::ofstream formStream(formulaFilename);
+    printDimacs(formStream, d_clauses, d_originalClauseIndices);
+    formStream.close();
+
+    std::ofstream dratStream(dratFilename);
+    dratStream << d_binaryDratProof.str();
+    dratStream.close();
+
+#if CVC4_USE_DRAT2ER
+    int dratTrimExitCode =
+        drat2er::drat_trim::OptimizeWithDratTrim(formulaFilename,
+                                                 dratFilename,
+                                                 optFormulaFilename,
+                                                 optDratFilename,
+                                                 drat2er::options::QUIET);
+    AlwaysAssert(
+        dratTrimExitCode == 0, "drat-trim exited with %d", dratTrimExitCode);
+#else
+    Unimplemented(
+        "Proof production when using CryptoMiniSat requires drat2er.\n"
+        "Run contrib/get-drat2er, reconfigure with --drat2er, and rebuild");
+#endif
+
+    d_binaryDratProof.str("");
+    Assert(d_binaryDratProof.str().size() == 0);
+
+    std::ifstream lratStream(optDratFilename);
+    std::copy(std::istreambuf_iterator<char>(lratStream),
+              std::istreambuf_iterator<char>(),
+              std::ostreambuf_iterator<char>(d_binaryDratProof));
+
+    if (options::bvOptimizeSatProof()
+        == theory::bv::BvOptimizeSatProof::BITVECTOR_OPTIMIZE_SAT_PROOF_FORMULA)
+    {
+      std::ifstream optFormulaStream{optFormulaFilename};
+      std::vector<prop::SatClause> core = parseDimacs(optFormulaStream);
+      optFormulaStream.close();
+
+      // Now we need to compute the clause indices for the UNSAT core. This is a
+      // bit difficult because drat-trim may have reordered clauses, and/or
+      // removed duplicate literals. We use literal sets as the canonical clause
+      // form.
+      std::unordered_map<
+          std::unordered_set<prop::SatLiteral, prop::SatLiteralHashFunction>,
+          ClauseId,
+          prop::SatClauseSetHashFunction>
+          cannonicalClausesToIndices;
+      for (const auto& kv : d_clauses)
+      {
+        cannonicalClausesToIndices.emplace(
+            std::unordered_set<prop::SatLiteral, prop::SatLiteralHashFunction>{
+                kv.second.begin(), kv.second.end()},
+            kv.first);
+      }
+
+      d_coreClauseIndices.clear();
+      std::unordered_set<prop::SatLiteral, prop::SatLiteralHashFunction>
+          coreClauseCanonical;
+      for (const prop::SatClause& coreClause : core)
+      {
+        coreClauseCanonical.insert(coreClause.begin(), coreClause.end());
+        d_coreClauseIndices.push_back(
+            cannonicalClausesToIndices.at(coreClauseCanonical));
+        coreClauseCanonical.clear();
+      }
+      Debug("bv::clausal") << "Optimizing the DRAT proof and the formula"
+                           << std::endl;
+    }
+    else
+    {
+      Debug("bv::clausal") << "Optimizing the DRAT proof but not the formula"
+                           << std::endl;
+      d_coreClauseIndices = d_originalClauseIndices;
+    }
+
+    Assert(d_coreClauseIndices.size() > 0);
+    remove(formulaFilename);
+    remove(dratFilename);
+    remove(optDratFilename);
+    remove(optFormulaFilename);
+    Debug("bv::clausal") << "Optimized DRAT" << std::endl;
+  }
+  else
+  {
+    Debug("bv::clausal") << "Not optimizing the formula or the DRAT proof"
+                         << std::endl;
+    d_coreClauseIndices = d_originalClauseIndices;
   }
 }
 
@@ -120,10 +249,9 @@ void LfscClausalBitVectorProof::printBBDeclarationAndCnf(std::ostream& os,
   d_cnfProof->printAtomMapping(d_atomsInBitblastingProof, os, paren, letMap);
 
   os << "\n;; BB-CNF proofs\n";
-  for (const auto& idAndClause : d_usedClauses)
+  for (const ClauseId id : d_coreClauseIndices)
   {
-    d_cnfProof->printCnfProofForClause(
-        idAndClause.first, &idAndClause.second, os, paren);
+    d_cnfProof->printCnfProofForClause(id, &d_clauses.at(id), os, paren);
   }
 }
 
@@ -137,13 +265,8 @@ void LfscDratBitVectorProof::printEmptyClauseProof(std::ostream& os,
   os << "\n;; Proof of input to SAT solver\n";
   os << "(@ proofOfSatInput ";
   paren << ")";
-  std::vector<ClauseId> usedIds;
-  usedIds.reserve(d_usedClauses.size());
-  for (const auto& idAnd : d_usedClauses)
-  {
-    usedIds.push_back(idAnd.first);
-  };
-  LFSCProofPrinter::printSatInputProof(usedIds, os, "bb");
+
+  LFSCProofPrinter::printSatInputProof(d_coreClauseIndices, os, "bb");
 
   os << "\n;; DRAT Proof Value\n";
   os << "(@ dratProof ";
@@ -166,19 +289,13 @@ void LfscLratBitVectorProof::printEmptyClauseProof(std::ostream& os,
   os << "\n;; Proof of input to SAT solver\n";
   os << "(@ proofOfCMap ";
   paren << ")";
-  std::vector<ClauseId> usedIds;
-  usedIds.reserve(d_usedClauses.size());
-  for (const auto& idAnd : d_usedClauses)
-  {
-    usedIds.push_back(idAnd.first);
-  };
-  LFSCProofPrinter::printCMapProof(usedIds, os, "bb");
+  LFSCProofPrinter::printCMapProof(d_coreClauseIndices, os, "bb");
 
   os << "\n;; DRAT Proof Value\n";
   os << "(@ lratProof ";
   paren << ")";
-  lrat::LratProof pf =
-      lrat::LratProof::fromDratProof(d_usedClauses, d_binaryDratProof.str());
+  lrat::LratProof pf = lrat::LratProof::fromDratProof(
+      d_clauses, d_coreClauseIndices, d_binaryDratProof.str());
   pf.outputAsLfsc(os);
   os << "\n";
 
@@ -194,8 +311,8 @@ void LfscErBitVectorProof::printEmptyClauseProof(std::ostream& os,
          "the BV theory should only be proving bottom directly in the eager "
          "bitblasting mode");
 
-  er::ErProof pf =
-      er::ErProof::fromBinaryDratProof(d_usedClauses, d_binaryDratProof.str());
+  er::ErProof pf = er::ErProof::fromBinaryDratProof(
+      d_clauses, d_coreClauseIndices, d_binaryDratProof.str());
 
   pf.outputAsLfsc(os);
 }
diff --git a/src/proof/clausal_bitvector_proof.h b/src/proof/clausal_bitvector_proof.h
index b10b1ad1c..a410b5b38 100644
--- a/src/proof/clausal_bitvector_proof.h
+++ b/src/proof/clausal_bitvector_proof.h
@@ -61,9 +61,16 @@ class ClausalBitVectorProof : public BitVectorProof
 
  protected:
   // A list of all clauses and their ids which are passed into the SAT solver
-  std::vector<std::pair<ClauseId, prop::SatClause>> d_usedClauses;
+  std::unordered_map<ClauseId, prop::SatClause> d_clauses{};
+  std::vector<ClauseId> d_originalClauseIndices{};
   // Stores the proof recieved from the SAT solver.
-  std::ostringstream d_binaryDratProof;
+  std::ostringstream d_binaryDratProof{};
+  std::vector<ClauseId> d_coreClauseIndices{};
+
+ private:
+  // Optimizes the DRAT proof stored in `d_binaryDratProof` and returns a list
+  // of clause actually needed to check that proof (a smaller UNSAT core)
+  void optimizeDratProof();
 };
 
 /**
diff --git a/src/proof/dimacs_printer.cpp b/src/proof/dimacs.cpp
index 04f880e11..cced98660 100644
--- a/src/proof/dimacs_printer.cpp
+++ b/src/proof/dimacs.cpp
@@ -1,5 +1,5 @@
 /*********************                                                        */
-/*! \file dimacs_printer.cpp
+/*! \file dimacs.cpp
  ** \verbatim
  ** Top contributors (to current version):
  **   Alex Ozdemir
@@ -14,7 +14,9 @@
  ** Defines serialization for SAT problems as DIMACS
  **/
 
-#include "proof/dimacs_printer.h"
+#include "proof/dimacs.h"
+
+#include "base/cvc4_assert.h"
 
 #include <iostream>
 
@@ -43,14 +45,15 @@ std::ostream& textOut(std::ostream& o, const prop::SatClause& c)
   return o << "0";
 }
 
-void printDimacs(
-    std::ostream& o,
-    const std::vector<std::pair<ClauseId, prop::SatClause>>& usedClauses)
+void printDimacs(std::ostream& o,
+                 const std::unordered_map<ClauseId, prop::SatClause>& clauses,
+                 const std::vector<ClauseId>& usedIndices)
 {
   size_t maxVar = 0;
-  for (const auto& c : usedClauses)
+  for (const ClauseId i : usedIndices)
   {
-    for (const auto& l : c.second)
+    const prop::SatClause& c = clauses.at(i);
+    for (const auto& l : c)
     {
       if (l.getSatVariable() + 1 > maxVar)
       {
@@ -58,10 +61,11 @@ void printDimacs(
       }
     }
   }
-  o << "p cnf " << maxVar << " " << usedClauses.size() << '\n';
-  for (const auto& idAndClause : usedClauses)
+  o << "p cnf " << maxVar << " " << usedIndices.size() << '\n';
+  for (const ClauseId i : usedIndices)
   {
-    for (const auto& l : idAndClause.second)
+    const prop::SatClause& c = clauses.at(i);
+    for (const auto& l : c)
     {
       if (l.isNegated())
       {
@@ -73,5 +77,44 @@ void printDimacs(
   }
 }
 
+std::vector<prop::SatClause> parseDimacs(std::istream& in)
+{
+  std::string tag;
+  uint64_t nVars;
+  uint64_t nClauses;
+
+  in >> tag;
+  Assert(in.good());
+  Assert(tag == "p");
+
+  in >> tag;
+  Assert(in.good());
+  Assert(tag == "cnf");
+
+  in >> nVars;
+  Assert(nVars >= 0);
+
+  in >> nClauses;
+  Assert(nClauses >= 0);
+
+  std::vector<prop::SatClause> cnf;
+  for (uint64_t i = 0; i < nClauses; ++i)
+  {
+    cnf.emplace_back();
+    int64_t lit;
+    in >> lit;
+    Assert(in.good());
+    while (lit != 0)
+    {
+      cnf.back().emplace_back(std::abs(lit) - 1, lit < 0);
+      in >> lit;
+      Assert(static_cast<uint64_t>(std::abs(lit)) <= nVars);
+      Assert(in.good());
+    }
+  }
+
+  return cnf;
+}
+
 }  // namespace proof
 }  // namespace CVC4
diff --git a/src/proof/dimacs_printer.h b/src/proof/dimacs.h
index 2ae4abefa..5956c5d26 100644
--- a/src/proof/dimacs_printer.h
+++ b/src/proof/dimacs.h
@@ -1,5 +1,5 @@
 /*********************                                                        */
-/*! \file dimacs_printer.h
+/*! \file dimacs.h
  ** \verbatim
  ** Top contributors (to current version):
  **   Alex Ozdemir
@@ -11,16 +11,17 @@
  **
  ** \brief DIMACS SAT Problem Format
  **
- ** Defines serialization for SAT problems as DIMACS
+ ** Defines serialization/deserialization for SAT problems as DIMACS
  **/
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__PROOF__DIMACS_PRINTER_H
-#define CVC4__PROOF__DIMACS_PRINTER_H
+#ifndef CVC4__PROOF__DIMACS_H
+#define CVC4__PROOF__DIMACS_H
 
 #include <iosfwd>
 #include <memory>
+#include <unordered_map>
 
 #include "proof/clause_id.h"
 #include "prop/sat_solver_types.h"
@@ -56,11 +57,13 @@ std::ostream& textOut(std::ostream& o, const prop::SatClause& c);
  * @param o where to print to
  * @param usedClauses the CNF formula
  */
-void printDimacs(
-    std::ostream& o,
-    const std::vector<std::pair<ClauseId, prop::SatClause>>& usedClauses);
+void printDimacs(std::ostream& o,
+                 const std::unordered_map<ClauseId, prop::SatClause>& clauses,
+                 const std::vector<ClauseId>& usedIndices);
+
+std::vector<prop::SatClause> parseDimacs(std::istream& i);
 
 }  // namespace proof
 }  // namespace CVC4
 
-#endif  // CVC4__PROOF__DIMACS_PRINTER_H
+#endif  // CVC4__PROOF__DIMACS_H
diff --git a/src/proof/er/er_proof.cpp b/src/proof/er/er_proof.cpp
index 22903c3c9..9160546f9 100644
--- a/src/proof/er/er_proof.cpp
+++ b/src/proof/er/er_proof.cpp
@@ -31,7 +31,7 @@
 
 #include "base/cvc4_assert.h"
 #include "base/map_util.h"
-#include "proof/dimacs_printer.h"
+#include "proof/dimacs.h"
 #include "proof/lfsc_proof_printer.h"
 #include "proof/proof_manager.h"
 
@@ -80,8 +80,10 @@ TraceCheckProof TraceCheckProof::fromText(std::istream& in)
   return pf;
 }
 
-ErProof ErProof::fromBinaryDratProof(const ClauseUseRecord& usedClauses,
-                                     const std::string& dratBinary)
+ErProof ErProof::fromBinaryDratProof(
+    const std::unordered_map<ClauseId, prop::SatClause>& clauses,
+    const std::vector<ClauseId>& usedIds,
+    const std::string& dratBinary)
 {
   std::ostringstream cmd;
   char formulaFilename[] = "/tmp/cvc4-dimacs-XXXXXX";
@@ -101,7 +103,7 @@ ErProof ErProof::fromBinaryDratProof(const ClauseUseRecord& usedClauses,
 
   // Write the formula
   std::ofstream formStream(formulaFilename);
-  printDimacs(formStream, usedClauses);
+  printDimacs(formStream, clauses, usedIds);
   formStream.close();
 
   // Write the (binary) DRAT proof
@@ -126,7 +128,8 @@ ErProof ErProof::fromBinaryDratProof(const ClauseUseRecord& usedClauses,
 
   // Parse the resulting TRACECHECK proof into an ER proof.
   std::ifstream tracecheckStream(tracecheckFilename);
-  ErProof proof(usedClauses, TraceCheckProof::fromText(tracecheckStream));
+  TraceCheckProof pf = TraceCheckProof::fromText(tracecheckStream);
+  ErProof proof(clauses, usedIds, std::move(pf));
   tracecheckStream.close();
 
   remove(formulaFilename);
@@ -136,17 +139,21 @@ ErProof ErProof::fromBinaryDratProof(const ClauseUseRecord& usedClauses,
   return proof;
 }
 
-ErProof::ErProof(const ClauseUseRecord& usedClauses,
+ErProof::ErProof(const std::unordered_map<ClauseId, prop::SatClause>& clauses,
+                 const std::vector<ClauseId>& usedIds,
                  TraceCheckProof&& tracecheck)
     : d_inputClauseIds(), d_definitions(), d_tracecheck(tracecheck)
 {
   // Step zero, save input clause Ids for future printing
-  std::transform(usedClauses.begin(),
-                 usedClauses.end(),
-                 std::back_inserter(d_inputClauseIds),
-                 [](const std::pair<ClauseId, prop::SatClause>& pair) {
-                   return pair.first;
-                 });
+  d_inputClauseIds = usedIds;
+
+  // Make a list of (idx, clause pairs), the used ones.
+  std::vector<std::pair<ClauseId, prop::SatClause>> usedClauses;
+  std::transform(
+      usedIds.begin(),
+      usedIds.end(),
+      std::back_inserter(usedClauses),
+      [&](const ClauseId& i) { return make_pair(i, clauses.at(i)); });
 
   // Step one, verify the formula starts the proof
   if (Configuration::isAssertionBuild())
@@ -162,14 +169,6 @@ ErProof::ErProof(const ClauseUseRecord& usedClauses,
           originalClause{usedClauses[i].second.begin(),
                          usedClauses[i].second.end()};
       Assert(traceCheckClause == originalClause);
-      Assert(d_tracecheck.d_lines[i].d_idx = i + 1);
-      Assert(d_tracecheck.d_lines[i].d_chain.size() == 0);
-      Assert(d_tracecheck.d_lines[i].d_clause.size()
-             == usedClauses[i].second.size());
-      for (size_t j = 0, m = usedClauses[i].second.size(); j < m; ++j)
-      {
-        Assert(usedClauses[i].second[j] == d_tracecheck.d_lines[i].d_clause[j]);
-      }
     }
   }
 
diff --git a/src/proof/er/er_proof.h b/src/proof/er/er_proof.h
index f5af0783b..d6cbd9213 100644
--- a/src/proof/er/er_proof.h
+++ b/src/proof/er/er_proof.h
@@ -27,6 +27,7 @@
 #define CVC4__PROOF__ER__ER_PROOF_H
 
 #include <memory>
+#include <unordered_map>
 #include <vector>
 
 #include "proof/clause_id.h"
@@ -36,8 +37,6 @@ namespace CVC4 {
 namespace proof {
 namespace er {
 
-using ClauseUseRecord = std::vector<std::pair<ClauseId, prop::SatClause>>;
-
 /**
  * A definition of the form:
  *    newVar <-> p v (~x_1 ^ ~x_2 ^ ... ^ ~x_n)
@@ -116,11 +115,14 @@ class ErProof
   /**
    * Construct an ER proof from a DRAT proof, using drat2er
    *
-   * @param usedClauses The CNF formula that we're deriving bottom from.
-   * @param dratBinary  The DRAT proof from the SAT solver, as a binary stream.
+   * @param clauses A store of clauses that might be in our formula
+   * @param usedIds the ids of clauses that are actually in our formula
+   * @param dratBinary  The DRAT proof from the SAT solver, as a binary stream
    */
-  static ErProof fromBinaryDratProof(const ClauseUseRecord& usedClauses,
-                                     const std::string& dratBinary);
+  static ErProof fromBinaryDratProof(
+      const std::unordered_map<ClauseId, prop::SatClause>& clauses,
+      const std::vector<ClauseId>& usedIds,
+      const std::string& dratBinary);
 
   /**
    * Construct an ER proof from a TRACECHECK ER proof
@@ -128,10 +130,13 @@ class ErProof
    * This basically just identifies groups of lines which correspond to
    * definitions, and extracts them.
    *
-   * @param usedClauses The CNF formula that we're deriving bottom from.
+   * @param clauses A store of clauses that might be in our formula
+   * @param usedIds the ids of clauses that are actually in our formula
    * @param tracecheck  The TRACECHECK proof, as a stream.
    */
-  ErProof(const ClauseUseRecord& usedClauses, TraceCheckProof&& tracecheck);
+  ErProof(const std::unordered_map<ClauseId, prop::SatClause>& clauses,
+          const std::vector<ClauseId>& usedIds,
+          TraceCheckProof&& tracecheck);
 
   /**
    * Write the ER proof as an LFSC value of type (holds cln).
diff --git a/src/proof/lrat/lrat_proof.cpp b/src/proof/lrat/lrat_proof.cpp
index a1939ec92..e414c64c9 100644
--- a/src/proof/lrat/lrat_proof.cpp
+++ b/src/proof/lrat/lrat_proof.cpp
@@ -26,7 +26,7 @@
 
 #include "base/cvc4_assert.h"
 #include "base/output.h"
-#include "proof/dimacs_printer.h"
+#include "proof/dimacs.h"
 #include "proof/lfsc_proof_printer.h"
 
 #if CVC4_USE_DRAT2ER
@@ -104,6 +104,7 @@ void printHints(std::ostream& o,
  */
 void printIndices(std::ostream& o, const std::vector<ClauseIdx>& indices)
 {
+  Assert(indices.size() > 0);
   // Verify that the indices are sorted!
   for (size_t i = 0, n = indices.size() - 1; i < n; ++i)
   {
@@ -123,7 +124,8 @@ void printIndices(std::ostream& o, const std::vector<ClauseIdx>& indices)
 // Prints the LRAT addition line in textual format
 
 LratProof LratProof::fromDratProof(
-    const std::vector<std::pair<ClauseId, prop::SatClause>>& usedClauses,
+    const std::unordered_map<ClauseId, prop::SatClause>& clauses,
+    const std::vector<ClauseId> usedIds,
     const std::string& dratBinary)
 {
   std::ostringstream cmd;
@@ -141,7 +143,7 @@ LratProof LratProof::fromDratProof(
   AlwaysAssert(r > 0);
   close(r);
   std::ofstream formStream(formulaFilename);
-  printDimacs(formStream, usedClauses);
+  printDimacs(formStream, clauses, usedIds);
   formStream.close();
 
   std::ofstream dratStream(dratFilename);
@@ -206,10 +208,13 @@ LratProof::LratProof(std::istream& textualProof)
         }
         clauses.push_back(di);
       }
-      std::sort(clauses.begin(), clauses.end());
-      std::unique_ptr<LratInstruction> instr(
-          new LratDeletion(clauseIdx, std::move(clauses)));
-      d_instructions.push_back(std::move(instr));
+      if (clauses.size() > 0)
+      {
+        std::sort(clauses.begin(), clauses.end());
+        std::unique_ptr<LratInstruction> instr(
+            new LratDeletion(clauseIdx, std::move(clauses)));
+        d_instructions.push_back(std::move(instr));
+      }
     }
     else
     {
diff --git a/src/proof/lrat/lrat_proof.h b/src/proof/lrat/lrat_proof.h
index 33b2fad3f..54db1837d 100644
--- a/src/proof/lrat/lrat_proof.h
+++ b/src/proof/lrat/lrat_proof.h
@@ -129,15 +129,13 @@ class LratProof
   /**
    * @brief Construct an LRAT proof from a DRAT proof, using drat-trim
    *
-   * @param usedClauses The CNF formula that we're deriving bottom from.
-   *                    It's a map because other parts of the system represent
-   *                    it this way.
-   * @param clauseOrder A record of the order in which those clauses were
-   *                    given to the SAT solver.
+   * @param clauses A store of clauses that might be in our formula
+   * @param usedIds the ids of clauses that are actually in our formula
    * @param dratBinary  The DRAT proof from the SAT solver, as a binary stream.
    */
   static LratProof fromDratProof(
-      const std::vector<std::pair<ClauseId, prop::SatClause>>& usedClauses,
+      const std::unordered_map<ClauseId, prop::SatClause>& clauses,
+      const std::vector<ClauseId> usedIds,
       const std::string& dratBinary);
   /**
    * @brief Construct an LRAT proof from its textual representation
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 66198946f..303295112 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -31,6 +31,7 @@
 
 #include "base/configuration.h"
 #include "base/configuration_private.h"
+#include "base/cvc4_check.h"
 #include "base/exception.h"
 #include "base/listener.h"
 #include "base/modal_exception.h"
@@ -888,6 +889,7 @@ SmtEngine::SmtEngine(ExprManager* em)
       d_earlyTheoryPP(true),
       d_globalNegation(false),
       d_status(),
+      d_expectedStatus(),
       d_replayStream(NULL),
       d_private(NULL),
       d_statisticsRegistry(NULL),
@@ -2420,7 +2422,7 @@ void SmtEngine::setInfo(const std::string& key, const CVC4::SExpr& value)
       throw OptionException("argument to (set-info :status ..) must be "
                             "`sat' or `unsat' or `unknown'");
     }
-    d_status = Result(s, d_filename);
+    d_expectedStatus = Result(s, d_filename);
     return;
   }
   throw UnrecognizedOptionException();
@@ -3747,6 +3749,13 @@ Result SmtEngine::checkSatisfiability(const vector<Expr>& assumptions,
 
     // Remember the status
     d_status = r;
+    if (!d_expectedStatus.isUnknown() && !d_status.isUnknown()
+        && d_status != d_expectedStatus)
+    {
+      CVC4_FATAL() << "Expected result " << d_expectedStatus << " but got "
+                   << d_status;
+    }
+    d_expectedStatus = Result();
 
     setProblemExtended(false);
 
@@ -4428,13 +4437,7 @@ void SmtEngine::checkProof()
 
   std::string logicString = d_logic.getLogicString();
 
-  if (!(
-          // Pure logics
-          logicString == "QF_UF" || logicString == "QF_AX"
-          || logicString == "QF_BV" ||
-          // Non-pure logics
-          logicString == "QF_AUF" || logicString == "QF_UFBV"
-          || logicString == "QF_ABV" || logicString == "QF_AUFBV"))
+  if (!(d_logic <= LogicInfo("QF_AUFBVLRA")))
   {
     // This logic is not yet supported
     Notice() << "Notice: no proof-checking for " << logicString << " proofs yet"
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 165e93997..5913716e6 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -263,6 +263,11 @@ class CVC4_PUBLIC SmtEngine {
   Result d_status;
 
   /**
+   * The expected status of the next satisfiability check.
+   */
+  Result d_expectedStatus;
+
+  /**
    * The input file name (if any) or the name set through setInfo (if any)
    */
   std::string d_filename;
diff --git a/src/smt/smt_engine.i b/src/smt/smt_engine.i
index c054cb666..4018cc3dc 100644
--- a/src/smt/smt_engine.i
+++ b/src/smt/smt_engine.i
@@ -42,6 +42,9 @@ SWIGEXPORT void JNICALL Java_edu_nyu_acsys_CVC4_SmtEngine_dlRef(JNIEnv* jenv, jc
       swigCPtr = 0;
     }
   }
+
+%template(Map_ExprExpr) std::map<CVC4::Expr, CVC4::Expr>;
+
 #endif // SWIGJAVA
 
 %ignore CVC4::SmtEngine::setLogic(const char*);
diff --git a/src/theory/fp/fp_converter.cpp b/src/theory/fp/fp_converter.cpp
index a69cf8c96..fbdce8cd5 100644
--- a/src/theory/fp/fp_converter.cpp
+++ b/src/theory/fp/fp_converter.cpp
@@ -157,17 +157,17 @@ symbolicRoundingMode traits::RTN(void) { return symbolicRoundingMode(0x08); };
 symbolicRoundingMode traits::RTZ(void) { return symbolicRoundingMode(0x10); };
 void traits::precondition(const bool b)
 {
-  Assert(b);
+  AlwaysAssert(b);
   return;
 }
 void traits::postcondition(const bool b)
 {
-  Assert(b);
+  AlwaysAssert(b);
   return;
 }
 void traits::invariant(const bool b)
 {
-  Assert(b);
+  AlwaysAssert(b);
   return;
 }
 
diff --git a/src/theory/logic_info.cpp b/src/theory/logic_info.cpp
index 1712bb30a..e21d1f630 100644
--- a/src/theory/logic_info.cpp
+++ b/src/theory/logic_info.cpp
@@ -17,9 +17,10 @@
  **/
 #include "theory/logic_info.h"
 
-#include <string>
 #include <cstring>
+#include <iostream>
 #include <sstream>
+#include <string>
 
 #include "base/cvc4_assert.h"
 #include "expr/kind.h"
@@ -207,13 +208,15 @@ bool LogicInfo::operator==(const LogicInfo& other) const {
 
   PrettyCheckArgument(d_sharingTheories == other.d_sharingTheories, *this,
                       "LogicInfo internal inconsistency");
+  bool res = d_cardinalityConstraints == other.d_cardinalityConstraints
+             && d_higherOrder == other.d_higherOrder;
   if(isTheoryEnabled(theory::THEORY_ARITH)) {
     return d_integers == other.d_integers && d_reals == other.d_reals
            && d_transcendentals == other.d_transcendentals
            && d_linear == other.d_linear
-           && d_differenceLogic == other.d_differenceLogic;
+           && d_differenceLogic == other.d_differenceLogic && res;
   } else {
-    return true;
+    return res;
   }
 }
 
@@ -227,13 +230,15 @@ bool LogicInfo::operator<=(const LogicInfo& other) const {
   }
   PrettyCheckArgument(d_sharingTheories <= other.d_sharingTheories, *this,
                       "LogicInfo internal inconsistency");
+  bool res = (!d_cardinalityConstraints || other.d_cardinalityConstraints)
+             && (!d_higherOrder || other.d_higherOrder);
   if(isTheoryEnabled(theory::THEORY_ARITH) && other.isTheoryEnabled(theory::THEORY_ARITH)) {
     return (!d_integers || other.d_integers) && (!d_reals || other.d_reals)
            && (!d_transcendentals || other.d_transcendentals)
            && (d_linear || !other.d_linear)
-           && (d_differenceLogic || !other.d_differenceLogic);
+           && (d_differenceLogic || !other.d_differenceLogic) && res;
   } else {
-    return true;
+    return res;
   }
 }
 
@@ -247,13 +252,15 @@ bool LogicInfo::operator>=(const LogicInfo& other) const {
   }
   PrettyCheckArgument(d_sharingTheories >= other.d_sharingTheories, *this,
                       "LogicInfo internal inconsistency");
+  bool res = (d_cardinalityConstraints || !other.d_cardinalityConstraints)
+             && (d_higherOrder || !other.d_higherOrder);
   if(isTheoryEnabled(theory::THEORY_ARITH) && other.isTheoryEnabled(theory::THEORY_ARITH)) {
     return (d_integers || !other.d_integers) && (d_reals || !other.d_reals)
            && (d_transcendentals || !other.d_transcendentals)
            && (!d_linear || other.d_linear)
-           && (!d_differenceLogic || other.d_differenceLogic);
+           && (!d_differenceLogic || other.d_differenceLogic) && res;
     } else {
-    return true;
+      return res;
   }
 }
 
diff --git a/src/util/floatingpoint.cpp b/src/util/floatingpoint.cpp
index 4aed27c30..f7e73ca4b 100644
--- a/src/util/floatingpoint.cpp
+++ b/src/util/floatingpoint.cpp
@@ -441,17 +441,17 @@ rm traits::RTZ(void) { return ::CVC4::roundTowardZero; };
 
 void traits::precondition(const prop &p)
 {
-  Assert(p);
+  AlwaysAssert(p);
   return;
 }
 void traits::postcondition(const prop &p)
 {
-  Assert(p);
+  AlwaysAssert(p);
   return;
 }
 void traits::invariant(const prop &p)
 {
-  Assert(p);
+  AlwaysAssert(p);
   return;
 }
 }
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 9a61514e3..2ec8b26c9 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -586,6 +586,7 @@ set(regress_0_tests
   regress0/printer/bv_consts_bin.smt2
   regress0/printer/bv_consts_dec.smt2
   regress0/printer/empty_symbol_name.smt2
+  regress0/printer/let_shadowing.smt2
   regress0/printer/tuples_and_records.cvc
   regress0/push-pop/boolean/fuzz_12.smt2
   regress0/push-pop/boolean/fuzz_13.smt2
@@ -826,6 +827,7 @@ set(regress_0_tests
   regress0/smt2output.smt2
   regress0/smtlib/get-unsat-assumptions.smt2
   regress0/smtlib/reason-unknown.smt2
+  regress0/smtlib/set-info-status.smt2
   regress0/strings/bug001.smt2
   regress0/strings/bug002.smt2
   regress0/strings/bug612.smt2
diff --git a/test/regress/regress0/bv/ackermann1.smt2 b/test/regress/regress0/bv/ackermann1.smt2
index 218fd746b..7fd76c8cc 100644
--- a/test/regress/regress0/bv/ackermann1.smt2
+++ b/test/regress/regress0/bv/ackermann1.smt2
@@ -3,7 +3,6 @@
 (set-logic QF_UFBV)
 (set-info :smt-lib-version 2.0)
 (set-info :category "crafted")
-(set-info :status unsat)
 (declare-fun v0 () (_ BitVec 4))
 (declare-fun f ((_ BitVec 4)) (_ BitVec 4))
 (declare-fun g ((_ BitVec 4)) (_ BitVec 4))
diff --git a/test/regress/regress0/bv/ackermann4.smt2 b/test/regress/regress0/bv/ackermann4.smt2
index cb8ad2e55..0c1e323d5 100644
--- a/test/regress/regress0/bv/ackermann4.smt2
+++ b/test/regress/regress0/bv/ackermann4.smt2
@@ -3,7 +3,6 @@
 (set-logic QF_UFBV)
 (set-info :smt-lib-version 2.0)
 (set-info :category "crafted")
-(set-info :status unsat)
 (declare-fun v0 () (_ BitVec 4))
 (declare-fun f ((_ BitVec 4)) (_ BitVec 4))
 (declare-fun g ((_ BitVec 4)) (_ BitVec 4))
diff --git a/test/regress/regress0/fmf/Arrow_Order-smtlib.778341.smt b/test/regress/regress0/fmf/Arrow_Order-smtlib.778341.smt
index bb2630b93..ab1e41360 100644
--- a/test/regress/regress0/fmf/Arrow_Order-smtlib.778341.smt
+++ b/test/regress/regress0/fmf/Arrow_Order-smtlib.778341.smt
@@ -1,7 +1,6 @@
 ; COMMAND-LINE: --finite-model-find
 ; EXPECT: unsat
 (benchmark Isabelle
-:status sat
 :logic AUFLIA
 :extrasorts ( S1 S2 S3 S4 S5 S6 S7 S8 S9 S10 S11 S12 S13 S14 S15 S16 S17 S18 S19 S20 S21 S22 S23 S24 S25 S26 S27 S28 S29 S30 S31 S32 S33 S34 S35 S36 S37)
 :extrafuns (
diff --git a/test/regress/regress0/lemmas/sc_init_frame_gap.induction.smt b/test/regress/regress0/lemmas/sc_init_frame_gap.induction.smt
index 170239e6f..a14c745a3 100644
--- a/test/regress/regress0/lemmas/sc_init_frame_gap.induction.smt
+++ b/test/regress/regress0/lemmas/sc_init_frame_gap.induction.smt
@@ -1,3 +1,4 @@
+; COMMAND-LINE: --no-check-proofs
 (benchmark sc_init_frame_gap.induction.smt
   :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/regress0/printer/let_shadowing.smt2 b/test/regress/regress0/printer/let_shadowing.smt2
new file mode 100644
index 000000000..3251e4e38
--- /dev/null
+++ b/test/regress/regress0/printer/let_shadowing.smt2
@@ -0,0 +1,15 @@
+; COMMAND-LINE: --dump raw-benchmark --preprocess-only
+; SCRUBBER: grep assert
+; EXPECT: (assert (let ((_let_1 (* x y))) (= _let_1 _let_1 _let_0)))
+; EXPECT: (assert (let ((_let_1 (and a b))) (= _let_1 _let_1 (forall ((_let_0 Int)) (= 0 _let_0) ))))
+; EXPECT: (assert (let ((_let_1 (and a b))) (= _let_1 _let_1 (forall ((x Int)) (forall ((y Int)) (let ((_let_2 (and b a))) (and _let_1 _let_2 _let_2 (= 0 _let_0))) ) ))))
+(set-logic NIA)
+(declare-const _let_0 Int)
+(declare-const x Int)
+(declare-const y Int)
+(declare-const a Bool)
+(declare-const b Bool)
+(assert (= (* x y) (* x y) _let_0))
+(assert (= (and a b) (and a b) (forall ((_let_0 Int)) (= 0 _let_0))))
+(assert (= (and a b) (and a b) (forall ((x Int)) (forall ((y Int)) (and (and a b) (and b a) (and b a) (= 0 _let_0))))))
+(check-sat)
diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvxor.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvxor.smt2
index ef41eecdd..69c5def65 100644
--- a/test/regress/regress0/quantifiers/qbv-test-invert-bvxor.smt2
+++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvxor.smt2
@@ -1,7 +1,6 @@
 ; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full
 ; EXPECT: unsat
 (set-logic BV)
-(set-info :status sat)
 (declare-fun a () (_ BitVec 8))
 
 (assert (forall ((x (_ BitVec 8))) (not (= (bvxor x a) (bvmul a a)))))
diff --git a/test/regress/regress0/sets/mar2014/sharing-preregister.smt2 b/test/regress/regress0/sets/mar2014/sharing-preregister.smt2
index d851ca35e..e3e88c65f 100644
--- a/test/regress/regress0/sets/mar2014/sharing-preregister.smt2
+++ b/test/regress/regress0/sets/mar2014/sharing-preregister.smt2
@@ -1,6 +1,5 @@
 ; EXPECT: unsat
 (set-logic QF_UFLIAFS)
-(set-info :status sat)
 (declare-fun a () Int)
 (declare-fun b () Int)
 (declare-fun x () (Set Int))
diff --git a/test/regress/regress0/smtlib/set-info-status.smt2 b/test/regress/regress0/smtlib/set-info-status.smt2
new file mode 100644
index 000000000..489d686b3
--- /dev/null
+++ b/test/regress/regress0/smtlib/set-info-status.smt2
@@ -0,0 +1,22 @@
+; EXPECT: (error "Cannot get an unsat core unless immediately preceded by UNSAT/VALID response.")
+; EXPECT: sat
+; EXPECT: sat
+; EXPECT: unsat
+; EXPECT-ERROR: Expected result unsat but got sat
+; ERROR-SCRUBBER: sed -e '/Fatal failure within.*/d'
+; EXIT: -6
+(set-option :incremental true)
+(set-option :produce-unsat-cores true)
+(set-logic QF_BV)
+(set-info :status unsat)
+(get-unsat-core)
+(set-info :status sat)
+(check-sat)
+(set-info :status sat)
+(check-sat)
+(push)
+(assert false)
+(check-sat)
+(pop)
+(set-info :status unsat)
+(check-sat)
diff --git a/test/regress/regress0/uflra/constants0.smt b/test/regress/regress0/uflra/constants0.smt
index b07a6bc4e..87d762e54 100644
--- a/test/regress/regress0/uflra/constants0.smt
+++ b/test/regress/regress0/uflra/constants0.smt
@@ -1,3 +1,4 @@
+; COMMAND-LINE: --no-check-proofs
 (benchmark mathsat
 :logic QF_UFLRA
 :status unsat 
@@ -12,4 +13,4 @@
      (implies (= (f 3) (f x)) (= (f 5) (f x)))
      (implies (= (f 3) (f y)) (= (f 5) (f y)))
 )
-)
\ No newline at end of file
+)
diff --git a/test/regress/regress0/uflra/pb_real_10_0200_10_22.smt b/test/regress/regress0/uflra/pb_real_10_0200_10_22.smt
index 4508d1f85..2c762a941 100644
--- a/test/regress/regress0/uflra/pb_real_10_0200_10_22.smt
+++ b/test/regress/regress0/uflra/pb_real_10_0200_10_22.smt
@@ -1,3 +1,4 @@
+; COMMAND-LINE: --no-check-proofs
 (benchmark mathsat
 :source { MathSat group }
 :logic QF_UFLRA
diff --git a/test/regress/regress0/uflra/pb_real_10_0200_10_26.smt b/test/regress/regress0/uflra/pb_real_10_0200_10_26.smt
index d0e9bfed6..84519b5cb 100644
--- a/test/regress/regress0/uflra/pb_real_10_0200_10_26.smt
+++ b/test/regress/regress0/uflra/pb_real_10_0200_10_26.smt
@@ -1,3 +1,4 @@
+; COMMAND-LINE: --no-check-proofs
 (benchmark mathsat
 :source { MathSat group }
 :logic QF_UFLRA
diff --git a/test/regress/regress1/lemmas/pursuit-safety-8.smt b/test/regress/regress1/lemmas/pursuit-safety-8.smt
index 5985c500b..efdbc017c 100644
--- a/test/regress/regress1/lemmas/pursuit-safety-8.smt
+++ b/test/regress/regress1/lemmas/pursuit-safety-8.smt
@@ -1,3 +1,4 @@
+; COMMAND-LINE: --no-check-proofs
 (benchmark pursuit_safety_8.smt
   :source {
 SAL benchmark suite.  Created at SRI by Bruno Dutertre, John Rushby, Maria
diff --git a/test/regress/regress1/lemmas/simple_startup_9nodes.abstract.base.smt b/test/regress/regress1/lemmas/simple_startup_9nodes.abstract.base.smt
index 506b99b46..ee04fbf34 100644
--- a/test/regress/regress1/lemmas/simple_startup_9nodes.abstract.base.smt
+++ b/test/regress/regress1/lemmas/simple_startup_9nodes.abstract.base.smt
@@ -1,3 +1,4 @@
+; COMMAND-LINE: --no-check-proofs
 (benchmark tta_startup
   :source { TTA Startup. Bruno Dutertre (bruno@csl.sri.com) }
 
diff --git a/test/regress/regress1/quantifiers/qbv-test-invert-bvcomp.smt2 b/test/regress/regress1/quantifiers/qbv-test-invert-bvcomp.smt2
index 3b55c0b9a..6bcc6501b 100644
--- a/test/regress/regress1/quantifiers/qbv-test-invert-bvcomp.smt2
+++ b/test/regress/regress1/quantifiers/qbv-test-invert-bvcomp.smt2
@@ -1,7 +1,6 @@
 ; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full
 ; EXPECT: unsat
 (set-logic BV)
-(set-info :status sat)
 (declare-fun a () (_ BitVec 8))
 (declare-fun b () (_ BitVec 8))
 (declare-fun c () (_ BitVec 1))
diff --git a/test/regress/regress1/quantifiers/qe.smt2 b/test/regress/regress1/quantifiers/qe.smt2
index 673ece05b..96cdd2497 100644
--- a/test/regress/regress1/quantifiers/qe.smt2
+++ b/test/regress/regress1/quantifiers/qe.smt2
@@ -1,7 +1,6 @@
 ; COMMAND-LINE:
 ; EXPECT: (not (>= (+ a (* (- 1) b)) 1))
 (set-logic LIA)
-(set-info :status unsat)
 (declare-fun a () Int)
 (declare-fun b () Int)
 (get-qe (exists ((x Int)) (and (<= a x) (<= x b))))
diff --git a/test/regress/regress2/arith/pursuit-safety-11.smt b/test/regress/regress2/arith/pursuit-safety-11.smt
index 1c12e0770..e6365f24c 100644
--- a/test/regress/regress2/arith/pursuit-safety-11.smt
+++ b/test/regress/regress2/arith/pursuit-safety-11.smt
@@ -1,3 +1,4 @@
+; COMMAND-LINE: --no-check-proofs
 (benchmark pursuit_safety_11.smt
   :source {
 SAL benchmark suite.  Created at SRI by Bruno Dutertre, John Rushby, Maria
diff --git a/test/regress/regress2/arith/pursuit-safety-12.smt b/test/regress/regress2/arith/pursuit-safety-12.smt
index 8f79b3d92..56ebea066 100644
--- a/test/regress/regress2/arith/pursuit-safety-12.smt
+++ b/test/regress/regress2/arith/pursuit-safety-12.smt
@@ -1,3 +1,4 @@
+; COMMAND-LINE: --no-check-proofs
 (benchmark pursuit_safety_12.smt
   :source {
 SAL benchmark suite.  Created at SRI by Bruno Dutertre, John Rushby, Maria
diff --git a/test/unit/proof/er_proof_black.h b/test/unit/proof/er_proof_black.h
index 1620bb113..9089cee5f 100644
--- a/test/unit/proof/er_proof_black.h
+++ b/test/unit/proof/er_proof_black.h
@@ -20,6 +20,7 @@
 #include <cctype>
 #include <iostream>
 #include <iterator>
+#include <unordered_map>
 #include <vector>
 
 #include "proof/clause_id.h"
@@ -44,6 +45,23 @@ class ErProofBlack : public CxxTest::TestSuite
   void testErTraceCheckOutputMedium();
 };
 
+/**
+ * @brief Add a new clause to the clause store and list of used clauses
+ *
+ * @param clauses the clause store
+ * @param usedIds the used clauses
+ * @param id the id of the new clause
+ * @param clause the clause itself
+ */
+void addClause(std::unordered_map<ClauseId, SatClause>& clauses,
+               std::vector<ClauseId>& usedIds,
+               ClauseId id,
+               SatClause&& clause)
+{
+  clauses.emplace(id, std::move(clause));
+  usedIds.push_back(id);
+}
+
 void ErProofBlack::testTraceCheckParse1Line()
 {
   std::string tracecheckText = "1 -2 3 0 4 2 0\n";
@@ -113,40 +131,56 @@ void ErProofBlack::testErTraceCheckParse()
   std::istringstream stream(tracecheckText);
   TraceCheckProof tc = TraceCheckProof::fromText(stream);
 
-  std::vector<std::pair<ClauseId, SatClause>> usedClauses;
-  usedClauses.emplace_back(
+  std::unordered_map<ClauseId, SatClause> clauses;
+  std::vector<ClauseId> usedIds;
+  addClause(
+      clauses,
+      usedIds,
       1,
       std::vector<SatLiteral>{
           SatLiteral(0, false), SatLiteral(1, false), SatLiteral(2, true)});
-  usedClauses.emplace_back(
+  addClause(
+      clauses,
+      usedIds,
       2,
       std::vector<SatLiteral>{
           SatLiteral(0, true), SatLiteral(1, true), SatLiteral(2, false)});
-  usedClauses.emplace_back(
+  addClause(
+      clauses,
+      usedIds,
       3,
       std::vector<SatLiteral>{
           SatLiteral(1, false), SatLiteral(2, false), SatLiteral(3, true)});
-  usedClauses.emplace_back(
+  addClause(
+      clauses,
+      usedIds,
       4,
       std::vector<SatLiteral>{
           SatLiteral(1, true), SatLiteral(2, true), SatLiteral(3, false)});
-  usedClauses.emplace_back(
-      5,
-      std::vector<SatLiteral>{
-          SatLiteral(0, true), SatLiteral(2, true), SatLiteral(3, true)});
-  usedClauses.emplace_back(
+  addClause(clauses,
+            usedIds,
+            5,
+            std::vector<SatLiteral>{
+                SatLiteral(0, true), SatLiteral(2, true), SatLiteral(3, true)});
+  addClause(
+      clauses,
+      usedIds,
       6,
       std::vector<SatLiteral>{
           SatLiteral(0, false), SatLiteral(2, false), SatLiteral(3, false)});
-  usedClauses.emplace_back(
+  addClause(
+      clauses,
+      usedIds,
       7,
       std::vector<SatLiteral>{
           SatLiteral(0, true), SatLiteral(1, false), SatLiteral(3, false)});
-  usedClauses.emplace_back(
+  addClause(
+      clauses,
+      usedIds,
       8,
       std::vector<SatLiteral>{
           SatLiteral(0, false), SatLiteral(1, true), SatLiteral(3, true)});
-  ErProof pf(usedClauses, std::move(tc));
+  ErProof pf(clauses, usedIds, std::move(tc));
 
   TS_ASSERT_EQUALS(pf.getInputClauseIds()[0], 1);
   TS_ASSERT_EQUALS(pf.getInputClauseIds()[7], 8);
@@ -161,13 +195,17 @@ void ErProofBlack::testErTraceCheckParse()
   TS_ASSERT_EQUALS(pf.getTraceCheckProof().d_lines[16].d_idx, 17);
 
   TS_ASSERT_EQUALS(pf.getTraceCheckProof().d_lines[0].d_clause.size(), 3);
-  TS_ASSERT_EQUALS(pf.getTraceCheckProof().d_lines[0].d_clause[0], SatLiteral(0, false));
-  TS_ASSERT_EQUALS(pf.getTraceCheckProof().d_lines[0].d_clause[1], SatLiteral(1, false));
-  TS_ASSERT_EQUALS(pf.getTraceCheckProof().d_lines[0].d_clause[2], SatLiteral(2, true));
+  TS_ASSERT_EQUALS(pf.getTraceCheckProof().d_lines[0].d_clause[0],
+                   SatLiteral(0, false));
+  TS_ASSERT_EQUALS(pf.getTraceCheckProof().d_lines[0].d_clause[1],
+                   SatLiteral(1, false));
+  TS_ASSERT_EQUALS(pf.getTraceCheckProof().d_lines[0].d_clause[2],
+                   SatLiteral(2, true));
   TS_ASSERT_EQUALS(pf.getTraceCheckProof().d_lines[0].d_chain.size(), 0);
 
   TS_ASSERT_EQUALS(pf.getTraceCheckProof().d_lines[16].d_clause.size(), 1);
-  TS_ASSERT_EQUALS(pf.getTraceCheckProof().d_lines[16].d_clause[0], SatLiteral(1, false));
+  TS_ASSERT_EQUALS(pf.getTraceCheckProof().d_lines[16].d_clause[0],
+                   SatLiteral(1, false));
   TS_ASSERT_EQUALS(pf.getTraceCheckProof().d_lines[16].d_chain.size(), 3);
   TS_ASSERT_EQUALS(pf.getTraceCheckProof().d_lines[16].d_chain[0], 3);
   TS_ASSERT_EQUALS(pf.getTraceCheckProof().d_lines[16].d_chain[1], 15);
@@ -198,40 +236,56 @@ void ErProofBlack::testErTraceCheckOutput()
   std::istringstream stream(tracecheckText);
   TraceCheckProof tc = TraceCheckProof::fromText(stream);
 
-  std::vector<std::pair<ClauseId, SatClause>> usedClauses;
-  usedClauses.emplace_back(
+  std::unordered_map<ClauseId, SatClause> clauses;
+  std::vector<ClauseId> usedIds;
+  addClause(
+      clauses,
+      usedIds,
       1,
       std::vector<SatLiteral>{
           SatLiteral(0, false), SatLiteral(1, false), SatLiteral(2, true)});
-  usedClauses.emplace_back(
+  addClause(
+      clauses,
+      usedIds,
       2,
       std::vector<SatLiteral>{
           SatLiteral(0, true), SatLiteral(1, true), SatLiteral(2, false)});
-  usedClauses.emplace_back(
+  addClause(
+      clauses,
+      usedIds,
       3,
       std::vector<SatLiteral>{
           SatLiteral(1, false), SatLiteral(2, false), SatLiteral(3, true)});
-  usedClauses.emplace_back(
+  addClause(
+      clauses,
+      usedIds,
       4,
       std::vector<SatLiteral>{
           SatLiteral(1, true), SatLiteral(2, true), SatLiteral(3, false)});
-  usedClauses.emplace_back(
-      5,
-      std::vector<SatLiteral>{
-          SatLiteral(0, true), SatLiteral(2, true), SatLiteral(3, true)});
-  usedClauses.emplace_back(
+  addClause(clauses,
+            usedIds,
+            5,
+            std::vector<SatLiteral>{
+                SatLiteral(0, true), SatLiteral(2, true), SatLiteral(3, true)});
+  addClause(
+      clauses,
+      usedIds,
       6,
       std::vector<SatLiteral>{
           SatLiteral(0, false), SatLiteral(2, false), SatLiteral(3, false)});
-  usedClauses.emplace_back(
+  addClause(
+      clauses,
+      usedIds,
       7,
       std::vector<SatLiteral>{
           SatLiteral(0, true), SatLiteral(1, false), SatLiteral(3, false)});
-  usedClauses.emplace_back(
+  addClause(
+      clauses,
+      usedIds,
       8,
       std::vector<SatLiteral>{
           SatLiteral(0, false), SatLiteral(1, true), SatLiteral(3, true)});
-  ErProof pf(usedClauses, std::move(tc));
+  ErProof pf(clauses, usedIds, std::move(tc));
 
   std::ostringstream lfsc;
   pf.outputAsLfsc(lfsc);
@@ -290,17 +344,17 @@ void ErProofBlack::testErTraceCheckOutputMedium()
       "7 -1  2  4 0 0\n"
       "8  1 -2 -4 0 0\n"
 
-      "9  5  2  4 0 0\n"    // Definition with 2 other variables
+      "9  5  2  4 0 0\n"  // Definition with 2 other variables
       "10 5  1  0 0\n"
       "11 2 -5 -1 0 0\n"
       "12 4 -5 -1 0 0\n"
 
-      "13 6  0 0\n"       // Definition with no other variables
+      "13 6  0 0\n"  // Definition with no other variables
       "14 6  -3  0 0\n"
 
-      "15 -3 4 0 11 1 10 7 4 0\n" // Chain w/ both def. and input clauses
+      "15 -3 4 0 11 1 10 7 4 0\n"  // Chain w/ both def. and input clauses
 
-      "16 -2 -4 0 2 5 8 0\n" // The useful bit of the proof
+      "16 -2 -4 0 2 5 8 0\n"  // The useful bit of the proof
       "17 4 3 0 7 2 6 0\n"
       "18 2 -3 0 7 5 1 0\n"
       "19 2 0 3 17 18 0\n"
@@ -309,40 +363,56 @@ void ErProofBlack::testErTraceCheckOutputMedium()
   std::istringstream stream(tracecheckText);
   TraceCheckProof tc = TraceCheckProof::fromText(stream);
 
-  std::vector<std::pair<ClauseId, SatClause>> usedClauses;
-  usedClauses.emplace_back(
+  std::unordered_map<ClauseId, SatClause> clauses;
+  std::vector<ClauseId> usedIds;
+  addClause(
+      clauses,
+      usedIds,
       1,
       std::vector<SatLiteral>{
           SatLiteral(0, false), SatLiteral(1, false), SatLiteral(2, true)});
-  usedClauses.emplace_back(
+  addClause(
+      clauses,
+      usedIds,
       2,
       std::vector<SatLiteral>{
           SatLiteral(0, true), SatLiteral(1, true), SatLiteral(2, false)});
-  usedClauses.emplace_back(
+  addClause(
+      clauses,
+      usedIds,
       3,
       std::vector<SatLiteral>{
           SatLiteral(1, false), SatLiteral(2, false), SatLiteral(3, true)});
-  usedClauses.emplace_back(
+  addClause(
+      clauses,
+      usedIds,
       4,
       std::vector<SatLiteral>{
           SatLiteral(1, true), SatLiteral(2, true), SatLiteral(3, false)});
-  usedClauses.emplace_back(
-      5,
-      std::vector<SatLiteral>{
-          SatLiteral(0, true), SatLiteral(2, true), SatLiteral(3, true)});
-  usedClauses.emplace_back(
+  addClause(clauses,
+            usedIds,
+            5,
+            std::vector<SatLiteral>{
+                SatLiteral(0, true), SatLiteral(2, true), SatLiteral(3, true)});
+  addClause(
+      clauses,
+      usedIds,
       6,
       std::vector<SatLiteral>{
           SatLiteral(0, false), SatLiteral(2, false), SatLiteral(3, false)});
-  usedClauses.emplace_back(
+  addClause(
+      clauses,
+      usedIds,
       7,
       std::vector<SatLiteral>{
           SatLiteral(0, true), SatLiteral(1, false), SatLiteral(3, false)});
-  usedClauses.emplace_back(
+  addClause(
+      clauses,
+      usedIds,
       8,
       std::vector<SatLiteral>{
           SatLiteral(0, false), SatLiteral(1, true), SatLiteral(3, true)});
-  ErProof pf(usedClauses, std::move(tc));
+  ErProof pf(clauses, usedIds, std::move(tc));
 
   std::ostringstream lfsc;
   pf.outputAsLfsc(lfsc);
diff --git a/test/unit/theory/logic_info_white.h b/test/unit/theory/logic_info_white.h
index b55197e50..2cc53bef3 100644
--- a/test/unit/theory/logic_info_white.h
+++ b/test/unit/theory/logic_info_white.h
@@ -732,6 +732,10 @@ public:
   }
 
   void testComparison() {
+    LogicInfo ufHo = LogicInfo("QF_UF").getUnlockedCopy();
+    ufHo.enableHigherOrder();
+    ufHo.lock();
+
     eq("QF_UF", "QF_UF");
     nc("QF_UF", "QF_LRA");
     nc("QF_UF", "QF_LIA");
@@ -756,6 +760,9 @@ public:
     lt("QF_UF", "AUFLIA");
     lt("QF_UF", "AUFLIRA");
     lt("QF_UF", "AUFNIRA");
+    lt("QF_UF", "QF_UFC");
+    lt("QF_UF", ufHo);
+    nc("QF_UFC", ufHo);
 
     nc("QF_LRA", "QF_UF");
     eq("QF_LRA", "QF_LRA");
@@ -781,6 +788,7 @@ public:
     nc("QF_LRA", "AUFLIA");
     lt("QF_LRA", "AUFLIRA");
     lt("QF_LRA", "AUFNIRA");
+    lt("QF_LRA", "QF_UFCLRA");
 
     nc("QF_LIA", "QF_UF");
     nc("QF_LIA", "QF_LRA");
@@ -1335,6 +1343,11 @@ public:
     gt("AUFNIRA", "AUFLIRA");
     eq("AUFNIRA", "AUFNIRA");
     lt("AUFNIRA", "AUFNIRAT");
+
+    gt("QF_UFC", "QF_UF");
+    gt("QF_UFCLRA", "QF_UFLRA");
+
+    gt(ufHo, "QF_UF");
   }
 
 };/* class LogicInfoWhite */