diff options
Diffstat (limited to 'src/theory/arrays/array_proof_reconstruction.cpp')
| -rw-r--r-- | src/theory/arrays/array_proof_reconstruction.cpp | 19 |
1 files changed, 14 insertions, 5 deletions
diff --git a/src/theory/arrays/array_proof_reconstruction.cpp b/src/theory/arrays/array_proof_reconstruction.cpp index c8a6716f5..11c3dc081 100644 --- a/src/theory/arrays/array_proof_reconstruction.cpp +++ b/src/theory/arrays/array_proof_reconstruction.cpp @@ -1,9 +1,18 @@ /********************* */ -/*! \file array_proof_reconstruction.h -** \verbatim -** -** \brief Array-specific proof construction logic to be used during the -** equality engine's path reconstruction +/*! \file array_proof_reconstruction.cpp + ** \verbatim + ** Top contributors (to current version): + ** Guy Katz + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2016 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 + ** + ** [[ Add lengthier description here ]] + + ** \todo document this file + **/ #include "theory/arrays/array_proof_reconstruction.h" |