Bitme header comment

tools/bitme.py

@@ -1,5 +1,24 @@
 #!/usr/bin/env python3
 
+# Copyright (c) the Selfie Project authors. All rights reserved.
+# Please see the AUTHORS file for details. Use of this source code is
+# governed by a BSD license that can be found in the LICENSE file.
+
+# Selfie is a project of the Computational Systems Group at the
+# Department of Computer Sciences of the University of Salzburg
+# in Austria. For further information and code please refer to:
+
+# selfie.cs.uni-salzburg.at
+
+# Bitme is a bounded model checker for BTOR2 models using
+# the Z3 and bitwuzla SMT solvers as reasoning engines.
+
+# Bitme is designed to work with BTOR2 models generated by rotor
+# for modeling RISC-V machines and RISC-V code. Rotor is a tool
+# that is part of the selfie system.
+
+# ------------------------------------------------------------
+
 # for debugging segfaults: import faulthandler; faulthandler.enable()
 
 # requires Z3 and the Z3 Python API:

tools/rotor.c

@@ -11,6 +11,7 @@ selfie.cs.uni-salzburg.at
 
 Rotor is a tool for bit-precise reasoning about RISC-V machines
 and RISC-V code using BTOR2 and SMT-LIB as modeling format.
+Rotor utilizes the compiler and bootloader of the selfie system.
 
 Rotor generates models of 64-bit and 32-bit RISC-V machines
 supporting 64-bit and 32-bit integer arithmetic (RV64I, RV32I)