diff --git a/src/sat/sat_cutset.cpp b/src/sat/sat_cutset.cpp
index e2f94f1c5..ab5005862 100644
--- a/src/sat/sat_cutset.cpp
+++ b/src/sat/sat_cutset.cpp
@@ -11,7 +11,6 @@
 
   --*/
 
-#pragma once;
 
 #include "util/hashtable.h"
 #include "sat/sat_cutset.h"
diff --git a/src/sat/sat_cutset.h b/src/sat/sat_cutset.h
index 9773eaf17..fd8b24548 100644
--- a/src/sat/sat_cutset.h
+++ b/src/sat/sat_cutset.h
@@ -1,3 +1,15 @@
+/*++
+  Copyright (c) 2020 Microsoft Corporation
+
+  Module Name:
+
+   sat_cutset.cpp
+
+  Author:
+
+    Nikolaj Bjorner 2020-01-02
+
+  --*/
 
 #pragma once;
 #include "util/region.h"
diff --git a/src/sat/sat_cutset_compute_shift.h b/src/sat/sat_cutset_compute_shift.h
index 09ca551bf..5222e704f 100644
--- a/src/sat/sat_cutset_compute_shift.h
+++ b/src/sat/sat_cutset_compute_shift.h
@@ -1,3 +1,24 @@
+/*++
+  Copyright (c) 2020 Microsoft Corporation
+
+  Module Name:
+
+   sat_cutset_compute_shift.h
+
+  Author:
+
+    Nikolaj Bjorner 2020-01-02
+
+  Notes:
+    
+    shifts truth table x using 'code'.
+    code encodes a mapping from bit-positions of the 
+    input truth table encoded with x into bit-positions
+    in the output truth table.
+    The truth table covers up to 6 inputs, which fits in 64 bits.
+
+  --*/
+
 static uint64_t compute_shift(uint64_t x, unsigned code) {
     switch (code) {
 #define _x0 (x & 1)