summaryrefslogtreecommitdiff
path: root/test/unit/proof/drat_proof_black.h
diff options
context:
space:
mode:
Diffstat (limited to 'test/unit/proof/drat_proof_black.h')
-rw-r--r--test/unit/proof/drat_proof_black.h8
1 files changed, 4 insertions, 4 deletions
diff --git a/test/unit/proof/drat_proof_black.h b/test/unit/proof/drat_proof_black.h
index 946597bea..6fdb55593 100644
--- a/test/unit/proof/drat_proof_black.h
+++ b/test/unit/proof/drat_proof_black.h
@@ -2,9 +2,9 @@
/*! \file drat_proof_black.h
** \verbatim
** Top contributors (to current version):
- ** Alex Ozdemir
+ ** Alex Ozdemir, Andres Noetzli
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
** in the top-level source directory) and their institutional affiliations.
** All rights reserved. See the file COPYING in the top-level source
** directory for licensing information.\endverbatim
@@ -170,8 +170,8 @@ void DratProofBlack::testOutputTwoAsLfsc()
}
}
std::string expectedLfsc =
- "(DRATProofd (clc (neg .v62) (clc (neg .v8192) cln))"
- "(DRATProofa (clc (pos .v128) (clc (neg .v8190) cln))"
+ "(DRATProofd (clc (neg bb.v62) (clc (neg bb.v8192) cln))"
+ "(DRATProofa (clc (pos bb.v128) (clc (neg bb.v8190) cln))"
"DRATProofn))";
std::ostringstream expectedLfscWithoutWhitespace;
for (char c : expectedLfsc)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback