From 9d0734cf73454ecfd51556ca84daaba9025b28f8 Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Mon, 9 Sep 2013 15:27:22 -0400
Subject: [PATCH] Fix some line-numbering in auto-generated metakind.h.  Thanks
 to Martin Brain for reporting this.

---
 src/expr/metakind_template.h | 1 +
 src/expr/mkmetakind          | 9 +++++----
 2 files changed, 6 insertions(+), 4 deletions(-)

diff --git a/src/expr/metakind_template.h b/src/expr/metakind_template.h
index 41813abde..e3f1b5c45 100644
--- a/src/expr/metakind_template.h
+++ b/src/expr/metakind_template.h
@@ -337,6 +337,7 @@ static inline Kind operatorToKind(::CVC4::expr::NodeValue* nv) {
 
   switch(Kind k CVC4_UNUSED = nv->getKind()) {
 ${metakind_operatorKinds}
+
   default:
     return kind::UNDEFINED_KIND;  /* LAST_KIND */
   };
diff --git a/src/expr/mkmetakind b/src/expr/mkmetakind
index d8192e432..7ffe0230b 100755
--- a/src/expr/mkmetakind
+++ b/src/expr/mkmetakind
@@ -303,8 +303,9 @@ struct ConstantMapReverse< ::CVC4::kind::$1 > {
 function registerOperatorToKind {
   operatorKind=$1
   applyKind=$2
-  metakind_operatorKinds="${metakind_operatorKinds}    case kind::$applyKind: return kind::$operatorKind;
-";
+  metakind_operatorKinds="${metakind_operatorKinds}
+#line $lineno \"$kf\"
+    case kind::$applyKind: return kind::$operatorKind;";
 }
 
 function register_metakind {
@@ -381,8 +382,8 @@ while [ $# -gt 0 ]; do
     /* from $b */
 "
   metakind_operatorKinds="${metakind_operatorKinds}
-    /* from $b */
-"
+
+    /* from $b */"
   source "$kf"
   if ! $seen_theory; then
     echo "$kf: error: no theory content found in file!" >&2
-- 
2.30.2