Implement alpha equivalence proofs (#7066)

This is a modified version of #6137 which accounts for extended rewriting between quantified formulas that are considered alpha equivalent.

It also generalizes the proof rule ALPHA_EQUIV. Notice that if we were to make this rule more pedantic, we would check for variable shadowing during substitution, although this is not currently done.

13 files changed, 299 insertions, 63 deletions

diff --git a/src/expr/term_canonize.cpp b/src/expr/term_canonize.cpp
index 0e05a52ea..5ab5a4b1b 100644
--- a/src/expr/term_canonize.cpp
+++ b/src/expr/term_canonize.cpp
@@ -222,5 +222,14 @@ Node TermCanonize::getCanonicalTerm(TNode n, bool apply_torder, bool doHoVar)
   return getCanonicalTerm(n, apply_torder, doHoVar, var_count, visited);
 }
 
+Node TermCanonize::getCanonicalTerm(TNode n,
+                                    std::map<TNode, Node>& visited,
+                                    bool apply_torder,
+                                    bool doHoVar)
+{
+  std::map<std::pair<TypeNode, uint32_t>, unsigned> var_count;
+  return getCanonicalTerm(n, apply_torder, doHoVar, var_count, visited);
+}
+
 }  // namespace expr
 }  // namespace cvc5
diff --git a/src/expr/term_canonize.h b/src/expr/term_canonize.h
index e1524cbf6..74eefdd2d 100644
--- a/src/expr/term_canonize.h
+++ b/src/expr/term_canonize.h
@@ -87,6 +87,14 @@ class TermCanonize
   Node getCanonicalTerm(TNode n,
                         bool apply_torder = false,
                         bool doHoVar = true);
+  /**
+   * Same as above but tracks visited map, mapping subterms of n to their
+   * canonical forms.
+   */
+  Node getCanonicalTerm(TNode n,
+                        std::map<TNode, Node>& visited,
+                        bool apply_torder = false,
+                        bool doHoVar = true);
 
  private:
   /** The (optional) type class callback */
diff --git a/src/proof/proof_rule.cpp b/src/proof/proof_rule.cpp
index acb49843f..5cf5dc0f8 100644
--- a/src/proof/proof_rule.cpp
+++ b/src/proof/proof_rule.cpp
@@ -135,6 +135,7 @@ const char* toString(PfRule id)
     case PfRule::EXISTS_INTRO: return "EXISTS_INTRO";
     case PfRule::SKOLEMIZE: return "SKOLEMIZE";
     case PfRule::INSTANTIATE: return "INSTANTIATE";
+    case PfRule::ALPHA_EQUIV: return "ALPHA_EQUIV";
     case PfRule::QUANTIFIERS_PREPROCESS: return "QUANTIFIERS_PREPROCESS";
     //================================================= String rules
     case PfRule::CONCAT_EQ: return "CONCAT_EQ";
diff --git a/src/proof/proof_rule.h b/src/proof/proof_rule.h
index 7b93e3a55..bb677bdb9 100644
--- a/src/proof/proof_rule.h
+++ b/src/proof/proof_rule.h
@@ -835,6 +835,17 @@ enum class PfRule : uint32_t
   // has prefix "QUANTIFIERS_INST_E_MATCHING", then t is the trigger that
   // generated the instantiation.
   INSTANTIATE,
+  // ======== Alpha equivalence
+  // Children: none
+  // Arguments: (F, (y1 = z1), ..., (yn = zn) )
+  // ----------------------------------------
+  // Conclusion: (= F F*sigma)
+  // sigma maps y1 ... yn to z1 ... zn, where y1 ... yn are unique bound
+  // variables, and z1 ... zn are unique bound variables. Notice that this
+  // rule is correct only when z1, ..., zn are not contained in
+  // FV(F) \ { y1 ... yn }. The internal quantifiers proof checker does not
+  // currently check that this is the case.
+  ALPHA_EQUIV,
   // ======== (Trusted) quantifiers preprocess
   // Children: ?
   // Arguments: (F)
@@ -842,7 +853,6 @@ enum class PfRule : uint32_t
   // Conclusion: F
   // where F is an equality of the form t = QuantifiersPreprocess::preprocess(t)
   QUANTIFIERS_PREPROCESS,
-
   //================================================= String rules
   //======================== Core solver
   // ======== Concat eq
diff --git a/src/theory/quantifiers/alpha_equivalence.cpp b/src/theory/quantifiers/alpha_equivalence.cpp
index 50b444b36..f4370c017 100644
--- a/src/theory/quantifiers/alpha_equivalence.cpp
+++ b/src/theory/quantifiers/alpha_equivalence.cpp
@@ -15,6 +15,10 @@
 
 #include "theory/quantifiers/alpha_equivalence.h"
 
+#include "proof/method_id.h"
+#include "proof/proof.h"
+#include "proof/proof_node.h"
+
 using namespace cvc5::kind;
 
 namespace cvc5 {
@@ -60,13 +64,62 @@ Node AlphaEquivalenceDb::addTerm(Node q)
   Assert(q.getKind() == FORALL);
   Trace("aeq") << "Alpha equivalence : register " << q << std::endl;
   //construct canonical quantified formula
-  Node t = d_tc->getCanonicalTerm(q[1], true);
+  Node t = d_tc->getCanonicalTerm(q[1], d_sortCommutativeOpChildren);
   Trace("aeq") << "  canonical form: " << t << std::endl;
+  return addTermToTypeTrie(t, q);
+}
+
+Node AlphaEquivalenceDb::addTermWithSubstitution(Node q,
+                                                 std::vector<Node>& vars,
+                                                 std::vector<Node>& subs)
+{
+  Trace("aeq") << "Alpha equivalence : register " << q << std::endl;
+  // construct canonical quantified formula with visited cache
+  std::map<TNode, Node> visited;
+  Node t = d_tc->getCanonicalTerm(q[1], visited, d_sortCommutativeOpChildren);
+  // only need to store BOUND_VARIABLE in substitution
+  std::map<Node, TNode>& bm = d_bvmap[q];
+  for (const std::pair<const TNode, Node>& b : visited)
+  {
+    if (b.first.getKind() == BOUND_VARIABLE)
+    {
+      Assert(b.second.getKind() == BOUND_VARIABLE);
+      bm[b.second] = b.first;
+    }
+  }
+  Node qret = addTermToTypeTrie(t, q);
+  if (qret != q)
+  {
+    Assert(d_bvmap.find(qret) != d_bvmap.end());
+    std::map<Node, TNode>& bmr = d_bvmap[qret];
+    std::map<Node, TNode>::iterator itb;
+    for (const std::pair<const Node, TNode>& b : bmr)
+    {
+      itb = bm.find(b.first);
+      if (itb == bm.end())
+      {
+        // didn't use the same variables, fail
+        vars.clear();
+        subs.clear();
+        break;
+      }
+      // otherwise, we map the variable in the returned quantified formula
+      // to the variable that used the same canonical variable
+      vars.push_back(b.second);
+      subs.push_back(itb->second);
+    }
+  }
+  return qret;
+}
+
+Node AlphaEquivalenceDb::addTermToTypeTrie(Node t, Node q)
+{
   //compute variable type counts
   std::map<TypeNode, size_t> typCount;
   std::vector< TypeNode > typs;
-  for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
-    TypeNode tn = q[0][i].getType();
+  for (const Node& v : q[0])
+  {
+    TypeNode tn = v.getType();
     typCount[tn]++;
     if( std::find( typs.begin(), typs.end(), tn )==typs.end() ){
       typs.push_back( tn );
@@ -81,33 +134,112 @@ Node AlphaEquivalenceDb::addTerm(Node q)
   return ret;
 }
 
-AlphaEquivalence::AlphaEquivalence() : d_termCanon(), d_aedb(&d_termCanon) {}
+AlphaEquivalence::AlphaEquivalence(Env& env)
+    : EnvObj(env),
+      d_termCanon(),
+      d_aedb(&d_termCanon, true),
+      d_pnm(env.getProofNodeManager()),
+      d_pfAlpha(d_pnm ? new EagerProofGenerator(d_pnm) : nullptr)
+{
+}
 
-Node AlphaEquivalence::reduceQuantifier(Node q)
+TrustNode AlphaEquivalence::reduceQuantifier(Node q)
 {
   Assert(q.getKind() == FORALL);
-  Trace("aeq") << "Alpha equivalence : register " << q << std::endl;
-  Node ret = d_aedb.addTerm(q);
+  Node ret;
+  std::vector<Node> vars;
+  std::vector<Node> subs;
+  if (isProofEnabled())
+  {
+    ret = d_aedb.addTermWithSubstitution(q, vars, subs);
+  }
+  else
+  {
+    ret = d_aedb.addTerm(q);
+  }
+  if (ret == q)
+  {
+    return TrustNode::null();
+  }
   Node lem;
-  if (ret != q)
+  ProofGenerator* pg = nullptr;
+  // lemma ( q <=> d_quant )
+  // Notice that we infer this equivalence regardless of whether q or ret
+  // have annotations (e.g. user patterns, names, etc.).
+  Trace("alpha-eq") << "Alpha equivalent : " << std::endl;
+  Trace("alpha-eq") << "  " << q << std::endl;
+  Trace("alpha-eq") << "  " << ret << std::endl;
+  lem = ret.eqNode(q);
+  if (q.getNumChildren() == 3)
   {
-    // lemma ( q <=> d_quant )
-    // Notice that we infer this equivalence regardless of whether q or ret
-    // have annotations (e.g. user patterns, names, etc.).
-    Trace("alpha-eq") << "Alpha equivalent : " << std::endl;
-    Trace("alpha-eq") << "  " << q << std::endl;
-    Trace("alpha-eq") << "  " << ret << std::endl;
-    lem = q.eqNode(ret);
-    if (q.getNumChildren() == 3)
+    Notice() << "Ignoring annotated quantified formula based on alpha "
+                "equivalence: "
+             << q << std::endl;
+  }
+  // if successfully computed the substitution above
+  if (isProofEnabled() && !vars.empty())
+  {
+    std::vector<Node> pfArgs;
+    pfArgs.push_back(ret);
+    for (size_t i = 0, nvars = vars.size(); i < nvars; i++)
+    {
+      pfArgs.push_back(vars[i].eqNode(subs[i]));
+      Trace("alpha-eq") << "subs: " << vars[i] << " -> " << subs[i]
+                        << std::endl;
+    }
+    CDProof cdp(d_pnm);
+    Node sret =
+        ret.substitute(vars.begin(), vars.end(), subs.begin(), subs.end());
+    std::vector<Node> transEq;
+    Node eq = ret.eqNode(sret);
+    transEq.push_back(eq);
+    // ---------- ALPHA_EQUIV
+    // ret = sret
+    cdp.addStep(eq, PfRule::ALPHA_EQUIV, {}, pfArgs);
+    // if not syntactically equal, maybe it can be transformed
+    bool success = false;
+    if (sret == q)
+    {
+      success = true;
+    }
+    else
+    {
+      Node eq2 = sret.eqNode(q);
+      transEq.push_back(eq2);
+      Node eq2r = extendedRewrite(eq2);
+      if (eq2r.isConst() && eq2r.getConst<bool>())
+      {
+        // ---------- MACRO_SR_PRED_INTRO
+        // sret = q
+        std::vector<Node> pfArgs2;
+        pfArgs2.push_back(eq2);
+        addMethodIds(pfArgs2,
+                     MethodId::SB_DEFAULT,
+                     MethodId::SBA_SEQUENTIAL,
+                     MethodId::RW_EXT_REWRITE);
+        cdp.addStep(eq2, PfRule::MACRO_SR_PRED_INTRO, {}, pfArgs2);
+        success = true;
+      }
+    }
+    // if successful, store the proof and remember the proof generator
+    if (success)
     {
-      Notice() << "Ignoring annotated quantified formula based on alpha "
-                  "equivalence: "
-               << q << std::endl;
+      if (transEq.size() > 1)
+      {
+        // TRANS of ALPHA_EQ and MACRO_SR_PRED_INTRO steps from above
+        cdp.addStep(lem, PfRule::TRANS, transEq, {});
+      }
+      std::shared_ptr<ProofNode> pn = cdp.getProofFor(lem);
+      Trace("alpha-eq") << "Proof is " << *pn.get() << std::endl;
+      d_pfAlpha->setProofFor(lem, pn);
+      pg = d_pfAlpha.get();
     }
   }
-  return lem;
+  return TrustNode::mkTrustLemma(lem, pg);
 }
 
+bool AlphaEquivalence::isProofEnabled() const { return d_pfAlpha != nullptr; }
+
 }  // namespace quantifiers
 }  // namespace theory
 }  // namespace cvc5
diff --git a/src/theory/quantifiers/alpha_equivalence.h b/src/theory/quantifiers/alpha_equivalence.h
index 886830229..d1a05e486 100644
--- a/src/theory/quantifiers/alpha_equivalence.h
+++ b/src/theory/quantifiers/alpha_equivalence.h
@@ -18,19 +18,20 @@
 #ifndef CVC5__ALPHA_EQUIVALENCE_H
 #define CVC5__ALPHA_EQUIVALENCE_H
 
-#include "theory/quantifiers/quant_util.h"
-
 #include "expr/term_canonize.h"
+#include "proof/eager_proof_generator.h"
+#include "smt/env_obj.h"
+#include "theory/quantifiers/quant_util.h"
 
 namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
 /**
- * This trie stores a trie of the above form for each multi-set of types. For
- * each term t registered to this node, we store t in the appropriate
- * AlphaEquivalenceNode trie. For example, if t contains 2 free variables
- * of type T1 and 3 free variables of type T2, then it is stored at
+ * This trie stores a trie for each multi-set of types. For each term t
+ * registered to this node, we store t in the appropriate
+ * AlphaEquivalenceTypeNode trie. For example, if t contains 2 free variables of
+ * type T1 and 3 free variables of type T2, then it is stored at
  * d_children[T1][2].d_children[T2][3].
  */
 class AlphaEquivalenceTypeNode {
@@ -59,7 +60,10 @@ public:
 class AlphaEquivalenceDb
 {
  public:
-  AlphaEquivalenceDb(expr::TermCanonize* tc) : d_tc(tc) {}
+  AlphaEquivalenceDb(expr::TermCanonize* tc, bool sortCommChildren)
+      : d_tc(tc), d_sortCommutativeOpChildren(sortCommChildren)
+  {
+  }
   /** adds quantified formula q to this database
    *
    * This function returns a quantified formula q' that is alpha-equivalent to
@@ -67,37 +71,65 @@ class AlphaEquivalenceDb
    * to addTerm.
    */
   Node addTerm(Node q);
+  /**
+   * Add term with substitution, which additionally finds a set of terms such
+   * that q' * subs is alpha-equivalent (possibly modulo rewriting) to q, where
+   * q' is the return quantified formula.
+   */
+  Node addTermWithSubstitution(Node q,
+                               std::vector<Node>& vars,
+                               std::vector<Node>& subs);
 
  private:
+  /**
+   * Add term to the trie, where t is the canonized form of the body of
+   * quantified formula q. Returns the quantified formula, if any, that already
+   * had been added to this class, or q otherwise.
+   */
+  Node addTermToTypeTrie(Node t, Node q);
   /** a trie per # of variables per type */
   AlphaEquivalenceTypeNode d_ae_typ_trie;
   /** pointer to the term canonize utility */
   expr::TermCanonize* d_tc;
+  /** whether to sort children of commutative operators during canonization. */
+  bool d_sortCommutativeOpChildren;
+  /**
+   * Maps quantified formulas to variables map, used for tracking substitutions
+   * in addTermWithSubstitution. The range in d_bvmap[q] contains the mapping
+   * from canonical free variables to variables in q.
+   */
+  std::map<Node, std::map<Node, TNode> > d_bvmap;
 };
 
 /**
  * A quantifiers module that computes reductions based on alpha-equivalence,
  * using the above utilities.
  */
-class AlphaEquivalence
+class AlphaEquivalence : protected EnvObj
 {
  public:
-  AlphaEquivalence();
+  AlphaEquivalence(Env& env);
   ~AlphaEquivalence(){}
   /** reduce quantifier
    *
-   * If non-null, its return value is lemma justifying why q is reducible.
-   * This is of the form ( q = q' ) where q' is a quantified formula that
-   * was previously registered to this class via a call to reduceQuantifier,
-   * and q and q' are alpha-equivalent.
+   * If non-null, its return value is a trust node containing the lemma
+   * justifying why q is reducible.  This lemma is of the form ( q = q' ) where
+   * q' is a quantified formula that was previously registered to this class via
+   * a call to reduceQuantifier, and q and q' are alpha-equivalent.
    */
-  Node reduceQuantifier( Node q );
+  TrustNode reduceQuantifier(Node q);
 
  private:
   /** a term canonizer */
   expr::TermCanonize d_termCanon;
   /** the database of quantified formulas registered to this class */
   AlphaEquivalenceDb d_aedb;
+  /** Pointer to the proof node manager */
+  ProofNodeManager* d_pnm;
+  /** An eager proof generator storing alpha equivalence proofs.*/
+  std::unique_ptr<EagerProofGenerator> d_pfAlpha;
+  /** Are proofs enabled for this object? */
+  bool isProofEnabled() const;
 };
 
 }
diff --git a/src/theory/quantifiers/proof_checker.cpp b/src/theory/quantifiers/proof_checker.cpp
index 5e02e16a5..c8ff49e11 100644
--- a/src/theory/quantifiers/proof_checker.cpp
+++ b/src/theory/quantifiers/proof_checker.cpp
@@ -32,6 +32,7 @@ void QuantifiersProofRuleChecker::registerTo(ProofChecker* pc)
   pc->registerChecker(PfRule::EXISTS_INTRO, this);
   pc->registerChecker(PfRule::SKOLEMIZE, this);
   pc->registerChecker(PfRule::INSTANTIATE, this);
+  pc->registerChecker(PfRule::ALPHA_EQUIV, this);
   // trusted rules
   pc->registerTrustedChecker(PfRule::QUANTIFIERS_PREPROCESS, this, 3);
 }
@@ -120,6 +121,41 @@ Node QuantifiersProofRuleChecker::checkInternal(
         body.substitute(vars.begin(), vars.end(), subs.begin(), subs.end());
     return inst;
   }
+  else if (id == PfRule::ALPHA_EQUIV)
+  {
+    Assert(children.empty());
+    if (args[0].getKind() != kind::FORALL)
+    {
+      return Node::null();
+    }
+    // arguments must be equalities that are bound variables that are
+    // pairwise unique
+    std::unordered_set<Node> allVars[2];
+    std::vector<Node> vars;
+    std::vector<Node> newVars;
+    for (size_t i = 1, nargs = args.size(); i < nargs; i++)
+    {
+      if (args[i].getKind() != kind::EQUAL)
+      {
+        return Node::null();
+      }
+      for (size_t j = 0; j < 2; j++)
+      {
+        Node v = args[i][j];
+        if (v.getKind() != kind::BOUND_VARIABLE
+            || allVars[j].find(v) != allVars[j].end())
+        {
+          return Node::null();
+        }
+        allVars[j].insert(v);
+      }
+      vars.push_back(args[i][0]);
+      newVars.push_back(args[i][1]);
+    }
+    Node renamedBody = args[0].substitute(
+        vars.begin(), vars.end(), newVars.begin(), newVars.end());
+    return args[0].eqNode(renamedBody);
+  }
   else if (id == PfRule::QUANTIFIERS_PREPROCESS)
   {
     Assert(!args.empty());
diff --git a/src/theory/quantifiers/quantifiers_modules.cpp b/src/theory/quantifiers/quantifiers_modules.cpp
index 563951189..f882daaba 100644
--- a/src/theory/quantifiers/quantifiers_modules.cpp
+++ b/src/theory/quantifiers/quantifiers_modules.cpp
@@ -96,7 +96,7 @@ void QuantifiersModules::initialize(Env& env,
   }
   if (options::quantAlphaEquiv())
   {
-    d_alpha_equiv.reset(new AlphaEquivalence());
+    d_alpha_equiv.reset(new AlphaEquivalence(env));
   }
   // full saturation : instantiate from relevant domain, then arbitrary terms
   if (options::fullSaturateQuant() || options::fullSaturateInterleave())
diff --git a/src/theory/quantifiers/quantifiers_modules.h b/src/theory/quantifiers/quantifiers_modules.h
index 9878e79ae..a7c8fc576 100644
--- a/src/theory/quantifiers/quantifiers_modules.h
+++ b/src/theory/quantifiers/quantifiers_modules.h
@@ -34,7 +34,7 @@
 
 namespace cvc5 {
 namespace theory {
-  
+
 class QuantifiersEngine;
 class DecisionManager;
 
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index b713dbec1..dfce485f2 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -507,37 +507,37 @@ void QuantifiersEngine::notifyCombineTheories() {
   // in quantifiers state.
 }
 
-bool QuantifiersEngine::reduceQuantifier( Node q ) {
-  //TODO: this can be unified with preregistration: AlphaEquivalence takes ownership of reducable quants
-  BoolMap::const_iterator it = d_quants_red.find( q );
-  if( it==d_quants_red.end() ){
-    Node lem;
+bool QuantifiersEngine::reduceQuantifier(Node q)
+{
+  // TODO: this can be unified with preregistration: AlphaEquivalence takes
+  // ownership of reducable quants
+  BoolMap::const_iterator it = d_quants_red.find(q);
+  if (it == d_quants_red.end())
+  {
+    TrustNode tlem;
     InferenceId id = InferenceId::UNKNOWN;
-    std::map< Node, Node >::iterator itr = d_quants_red_lem.find( q );
-    if( itr==d_quants_red_lem.end() ){
-      if (d_qmodules->d_alpha_equiv)
+    if (d_qmodules->d_alpha_equiv)
+    {
+      Trace("quant-engine-red")
+          << "Alpha equivalence " << q << "?" << std::endl;
+      // add equivalence with another quantified formula
+      tlem = d_qmodules->d_alpha_equiv->reduceQuantifier(q);
+      id = InferenceId::QUANTIFIERS_REDUCE_ALPHA_EQ;
+      if (!tlem.isNull())
       {
-        Trace("quant-engine-red") << "Alpha equivalence " << q << "?" << std::endl;
-        //add equivalence with another quantified formula
-        lem = d_qmodules->d_alpha_equiv->reduceQuantifier(q);
-        id = InferenceId::QUANTIFIERS_REDUCE_ALPHA_EQ;
-        if( !lem.isNull() ){
-          Trace("quant-engine-red") << "...alpha equivalence success." << std::endl;
-          ++(d_qstate.getStats().d_red_alpha_equiv);
-        }
+        Trace("quant-engine-red")
+            << "...alpha equivalence success." << std::endl;
+        ++(d_qstate.getStats().d_red_alpha_equiv);
       }
-      d_quants_red_lem[q] = lem;
-    }else{
-      lem = itr->second;
     }
-    if( !lem.isNull() ){
-      d_qim.lemma(lem, id);
+    if (!tlem.isNull())
+    {
+      d_qim.trustedLemma(tlem, id);
     }
-    d_quants_red[q] = !lem.isNull();
-    return !lem.isNull();
-  }else{
-    return (*it).second;
+    d_quants_red[q] = !tlem.isNull();
+    return !tlem.isNull();
   }
+  return (*it).second;
 }
 
 void QuantifiersEngine::registerQuantifierInternal(Node f)
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index e8c385fcd..547c30797 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -210,7 +210,6 @@ public:
   NodeSet d_quants_prereg;
   /** quantifiers reduced */
   BoolMap d_quants_red;
-  std::map<Node, Node> d_quants_red_lem;
   /** Number of rounds we have instantiated */
   uint32_t d_numInstRoundsLemma;
 }; /* class QuantifiersEngine */
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 176dadb40..55b932f81 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1750,6 +1750,7 @@ set(regress_1_tests
   regress1/proofs/issue6625-unsat-core-proofs.smt2
   regress1/proofs/macro-res-exp-crowding-lit-inside-unit.smt2
   regress1/proofs/macro-res-exp-singleton-after-elimCrowd.smt2
+  regress1/proofs/quant-alpha-eq.smt2
   regress1/proofs/sat-trivial-cycle.smt2
   regress1/proofs/unsat-cores-proofs.smt2
   regress1/push-pop/arith_lra_01.smt2
diff --git a/test/regress/regress1/proofs/quant-alpha-eq.smt2 b/test/regress/regress1/proofs/quant-alpha-eq.smt2
new file mode 100644
index 000000000..f804df43f
--- /dev/null
+++ b/test/regress/regress1/proofs/quant-alpha-eq.smt2
@@ -0,0 +1,8 @@
+(set-logic AUFLIA)
+(set-info :status unsat)
+(declare-sort A$ 0)
+(declare-fun p$ (A$) Bool)
+(assert (exists ((?v0 A$)) (p$ ?v0)))
+(assert (forall ((?v0 A$)) (not (p$ ?v0))))
+(assert (not false))
+(check-sat)