diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2019-10-15 14:43:33 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-10-15 14:43:33 -0700 |
| commit | 80b14c0965678fb91467de287b00a9a1d8a39be5 (patch) | |
| tree | 34d3da127ab61bc9adfff4b0298dc4f4c153d1be /src/expr/expr_template.h | |
| parent | c5eb0c1900e8cf12a18d15d8b1c0660c626bf137 (diff) | |
Fix line numbers in templates (#3391)
This commit updates the line numbers in templates to address warnings
due to wrong line numbers.
Diffstat (limited to 'src/expr/expr_template.h')
| -rw-r--r-- | src/expr/expr_template.h | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h index 4ca22459b..546a0d00e 100644 --- a/src/expr/expr_template.h +++ b/src/expr/expr_template.h @@ -621,7 +621,7 @@ private: ${getConst_instantiations} -#line 609 "${template}" +#line 625 "${template}" inline size_t ExprHashFunction::operator()(CVC4::Expr e) const { return (size_t) e.getId(); |