From 5ffe05a0b2769ba0b4b338b19e21c818bc1047a7 Mon Sep 17 00:00:00 2001
From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Mon, 26 Jul 2021 20:49:16 -0500
Subject: Miscellaneous sync to master

---
 src/proof/proof_letify.h                               | 1 -
 test/regress/regress0/bv/bv_to_int_bvmul2.smt2         | 6 +++---
 test/regress/regress0/fmf/sort-infer-typed-082718.smt2 | 1 +
 test/regress/regress0/proofs/scope.smt2                | 2 +-
 test/regress/regress2/instance_1444.smtv1.smt2         | 1 -
 5 files changed, 5 insertions(+), 6 deletions(-)

diff --git a/src/proof/proof_letify.h b/src/proof/proof_letify.h
index 71e174ab1..cfe1259e5 100644
--- a/src/proof/proof_letify.h
+++ b/src/proof/proof_letify.h
@@ -49,7 +49,6 @@ class ProofLetifyTraverseCallback
 class ProofLetify
 {
  public:
-  //------------------- letification of proofs
   /**
    * Stores proofs in map that require letification, mapping them to a unique
    * identifier. For each proof node in the domain of pletMap in the list
diff --git a/test/regress/regress0/bv/bv_to_int_bvmul2.smt2 b/test/regress/regress0/bv/bv_to_int_bvmul2.smt2
index ebec5169a..91e0c45fd 100644
--- a/test/regress/regress0/bv/bv_to_int_bvmul2.smt2
+++ b/test/regress/regress0/bv/bv_to_int_bvmul2.smt2
@@ -2,9 +2,9 @@
 ; EXPECT: unsat
 (set-logic QF_BV)
 (declare-fun T4_180 () (_ BitVec 32))
-(assert (and
-(= (bvmul T4_180 (_ bv1056 32)) (_ bv0 32))
-(not (= (bvmul T4_180 (_ bv1408 32)) (_ bv0 32)))
+(assert (and 
+(= (bvmul T4_180 (_ bv1056 32)) (_ bv0 32)) 
+(not (= (bvmul T4_180 (_ bv1408 32)) (_ bv0 32))) 
 )
 )
 (check-sat)
diff --git a/test/regress/regress0/fmf/sort-infer-typed-082718.smt2 b/test/regress/regress0/fmf/sort-infer-typed-082718.smt2
index 3e837cc73..9ee1fa5eb 100644
--- a/test/regress/regress0/fmf/sort-infer-typed-082718.smt2
+++ b/test/regress/regress0/fmf/sort-infer-typed-082718.smt2
@@ -3,3 +3,4 @@
 (set-logic ALL)
 (assert (not (exists ((X Int)) (not (= X 12)) )))
 (check-sat)
+
diff --git a/test/regress/regress0/proofs/scope.smt2 b/test/regress/regress0/proofs/scope.smt2
index 133dd0c34..7a324952e 100644
--- a/test/regress/regress0/proofs/scope.smt2
+++ b/test/regress/regress0/proofs/scope.smt2
@@ -51,4 +51,4 @@
 (assert (! (= (f2$ x2$ x4$) (f2$ (f5a$ x9$ x10$) x3$)) :named a7))
 (assert (! (not false) :named a8))
 (check-sat)
-(get-proof)
+(get-proof)
\ No newline at end of file
diff --git a/test/regress/regress2/instance_1444.smtv1.smt2 b/test/regress/regress2/instance_1444.smtv1.smt2
index b752b7838..47d3fda52 100644
--- a/test/regress/regress2/instance_1444.smtv1.smt2
+++ b/test/regress/regress2/instance_1444.smtv1.smt2
@@ -1,5 +1,4 @@
 ; COMMAND-LINE: --no-produce-proofs
-; EXPECT: unsat
 (set-option :incremental false)
 (set-info :status unsat)
 (set-logic QF_UF)
-- 
cgit v1.2.3