Fix some line-numbering in auto-generated metakind.h. Thanks to Martin Brain for...

diff --git a/src/expr/metakind_template.h b/src/expr/metakind_template.h
index 41813abded2c4d9cf7a15de55d05998bc15958fb..e3f1b5c4530095fea28bb6bae9baf6d0d7b4a09d 100644 (file)
--- 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 d8192e43228c59a58a471b4834e7c54530c7e0a6..7ffe0230b30728bb9cba0cd6b94bbe90ffd42b2f 100755 (executable)
--- 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