From a9a5a69b73d1f8125109ff606c33d32eae0e4166 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 9 Jul 2015 13:31:22 -0700
Subject: [PATCH] remove double underscores

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 scripts/update_header_guards.py | 18 +++++++++++++++---
 src/api/z3.h                    |  4 ++--
 src/api/z3_private.h            |  4 ++--
 src/ast/scoped_proof.h          |  4 ++--
 src/muz/ddnf/ddnf.h             |  4 ++--
 5 files changed, 23 insertions(+), 11 deletions(-)

diff --git a/scripts/update_header_guards.py b/scripts/update_header_guards.py
index 1cb2ae186..8af89ebea 100644
--- a/scripts/update_header_guards.py
+++ b/scripts/update_header_guards.py
@@ -3,9 +3,11 @@
 import os
 import re
 
-ifndef = re.compile("#ifndef \_(.*)\_H\_")
-defn   = re.compile("#define \_(.*)\_H\_")
-endif  = re.compile("#endif /\* \_(.*)\_H\_")
+ifndef  = re.compile("#ifndef \_(.*)\_H\_")
+doubleu = re.compile("#(.*) (.*)\_\_H\_")
+#doubleu2 = re.compile("#define (.*)\_\_H\_")
+defn    = re.compile("#define \_(.*)\_H\_")
+endif   = re.compile("#endif /\* \_(.*)\_H\_")
 
 
 def fix_hdr(file):
@@ -16,6 +18,16 @@ def fix_hdr(file):
     line = ins.readline()
     found = False
     while line:
+	m = doubleu.search(line)
+	if m:
+	    ous.write("#")
+	    ous.write(m.group(1))
+	    ous.write(" ")
+	    ous.write(m.group(2))
+	    ous.write("_H_\n")
+	    line = ins.readline()
+	    found = True
+	    continue	    
 	m = ifndef.search(line)
 	if m:
 	    print m.group(1)
diff --git a/src/api/z3.h b/src/api/z3.h
index 84037ab67..a096cb7ca 100644
--- a/src/api/z3.h
+++ b/src/api/z3.h
@@ -18,8 +18,8 @@ Notes:
     
 --*/
 
-#ifndef Z3__H_
-#define Z3__H_
+#ifndef Z3_H_
+#define Z3_H_
 
 #include<stdio.h>
 #include"z3_macros.h"
diff --git a/src/api/z3_private.h b/src/api/z3_private.h
index 3cfda6c72..5c5ee85a4 100644
--- a/src/api/z3_private.h
+++ b/src/api/z3_private.h
@@ -22,8 +22,8 @@ Notes:
 #include"rational.h"
 #include"z3_macros.h"
 
-#ifndef Z3_PRIVATE__H_
-#define Z3_PRIVATE__H_
+#ifndef Z3_PRIVATE_H_
+#define Z3_PRIVATE_H_
 
 
 #ifndef CAMLIDL
diff --git a/src/ast/scoped_proof.h b/src/ast/scoped_proof.h
index 5f0f86b44..2bbba5122 100644
--- a/src/ast/scoped_proof.h
+++ b/src/ast/scoped_proof.h
@@ -16,8 +16,8 @@ Author:
 Revision History:
 
 --*/
-#ifndef SCOPED_PROOF__H_
-#define SCOPED_PROOF__H_
+#ifndef SCOPED_PROOF_H_
+#define SCOPED_PROOF_H_
 
 #include "ast.h"
 
diff --git a/src/muz/ddnf/ddnf.h b/src/muz/ddnf/ddnf.h
index 63c275194..7e1e83e52 100644
--- a/src/muz/ddnf/ddnf.h
+++ b/src/muz/ddnf/ddnf.h
@@ -16,8 +16,8 @@ Author:
 Revision History:
 
 --*/
-#ifndef DDNF__H_
-#define DDNF__H_
+#ifndef DDNF_H_
+#define DDNF_H_
 
 #include "ast.h"
 #include "lbool.h"