4 files changed, 53 insertions, 6 deletions
diff --git a/src/proof/bitvector_proof.cpp b/src/proof/bitvector_proof.cpp
index 3fe426f15..b2d6fdecf 100644
--- a/src/proof/bitvector_proof.cpp
+++ b/src/proof/bitvector_proof.cpp
@@ -1000,4 +1000,34 @@ bool LFSCBitVectorProof::hasAlias(Expr expr) {
   return d_assignedAliases.find(expr) != d_assignedAliases.end();
 }
 
+void LFSCBitVectorProof::printConstantDisequalityProof(std::ostream& os, Expr c1, Expr c2) {
+  Assert (c1.isConst());
+  Assert (c2.isConst());
+  Assert (utils::getSize(c1) == utils::getSize(c2));
+
+  os << "(bv_disequal_constants " << utils::getSize(c1) << " ";
+
+  std::ostringstream paren;
+
+  for (int i = utils::getSize(c1) - 1; i >= 0; --i) {
+    os << "(bvc ";
+    os << (utils::getBit(c1, i) ? "b1" : "b0") << " ";
+    paren << ")";
+  }
+  os << "bvn";
+  os << paren.str();
+
+  os << " ";
+
+  for (int i = utils::getSize(c2) - 1; i >= 0; --i) {
+    os << "(bvc ";
+    os << (utils::getBit(c2, i) ? "b1" : "b0") << " ";
+
+  }
+  os << "bvn";
+  os << paren.str();
+
+  os << ")";
+}
+
 } /* namespace CVC4 */
diff --git a/src/proof/bitvector_proof.h b/src/proof/bitvector_proof.h
index 4e5e98541..5ea754e08 100644
--- a/src/proof/bitvector_proof.h
+++ b/src/proof/bitvector_proof.h
@@ -147,6 +147,7 @@ public:
   virtual void printAliasingDeclarations(std::ostream& os, std::ostream& paren);
   virtual void printBitblasting(std::ostream& os, std::ostream& paren);
   virtual void printResolutionProof(std::ostream& os, std::ostream& paren);
+  void printConstantDisequalityProof(std::ostream& os, Expr c1, Expr c2);
 };
 
 }/* CVC4 namespace */
diff --git a/src/proof/theory_proof.cpp b/src/proof/theory_proof.cpp
index eaf21846b..fe67ec94d 100644
--- a/src/proof/theory_proof.cpp
+++ b/src/proof/theory_proof.cpp
@@ -114,13 +114,11 @@ void TheoryProofEngine::markTermForFutureRegistration(Expr term, theory::TheoryI
 }
 
 void TheoryProofEngine::printConstantDisequalityProof(std::ostream& os, Expr c1, Expr c2) {
-  LetMap emptyMap;
+  Assert(c1.isConst());
+  Assert(c2.isConst());
 
-  os << "(trust_f (not (= _ ";
-  printBoundTerm(c1, os, emptyMap);
-  os << " ";
-  printBoundTerm(c2, os, emptyMap);
-  os << ")))";
+  Assert(theory::Theory::theoryOf(c1) == theory::Theory::theoryOf(c2));
+  getTheoryProof(theory::Theory::theoryOf(c1))->printConstantDisequalityProof(os, c1, c2);
 }
 
 void TheoryProofEngine::registerTerm(Expr term) {
@@ -1100,4 +1098,16 @@ void LFSCBooleanProof::printTheoryLemmaProof(std::vector<Expr>& lemma,
   Unreachable("No boolean lemmas yet!");
 }
 
+void TheoryProof::printConstantDisequalityProof(std::ostream& os, Expr c1, Expr c2) {
+  // By default, we just print a trust statement. Specific theories can implement
+  // better proofs.
+  LetMap emptyMap;
+
+  os << "(trust_f (not (= _ ";
+  d_proofEngine->printBoundTerm(c1, os, emptyMap);
+  os << " ";
+  d_proofEngine->printBoundTerm(c2, os, emptyMap);
+  os << ")))";
+}
+
 } /* namespace CVC4 */
diff --git a/src/proof/theory_proof.h b/src/proof/theory_proof.h
index c8c776ec9..352cc1b53 100644
--- a/src/proof/theory_proof.h
+++ b/src/proof/theory_proof.h
@@ -315,6 +315,12 @@ public:
    * @param term
    */
   virtual void registerTerm(Expr term) = 0;
+  /**
+   * Print a proof for the disequality of two constants that belong to this theory.
+   *
+   * @param term
+   */
+  virtual void printConstantDisequalityProof(std::ostream& os, Expr c1, Expr c2);
 
   virtual void treatBoolsAsFormulas(bool value) {}
 };