From aec6e8eb67e5f243d7fbc13502a727e2094fd9e6 Mon Sep 17 00:00:00 2001
From: FedericoAureliano <fmorarocha@gmail.com>
Date: Fri, 1 Nov 2024 18:43:30 -0700
Subject: [PATCH] fix bug in file names

---
 .../Backend/Uclid5/Uclid5CodeGenerator.cs       | 17 +++++++----------
 .../TypeChecker/DeclarationStubVisitor.cs       |  4 ++++
 2 files changed, 11 insertions(+), 10 deletions(-)

diff --git a/Src/PCompiler/CompilerCore/Backend/Uclid5/Uclid5CodeGenerator.cs b/Src/PCompiler/CompilerCore/Backend/Uclid5/Uclid5CodeGenerator.cs
index bef11ca44..c4d8da17b 100644
--- a/Src/PCompiler/CompilerCore/Backend/Uclid5/Uclid5CodeGenerator.cs
+++ b/Src/PCompiler/CompilerCore/Backend/Uclid5/Uclid5CodeGenerator.cs
@@ -63,7 +63,7 @@ public void Compile(ICompilerConfiguration job)
 
         foreach (var cmd in _commands)
         {
-            if (cmd.Name == "default")
+            if (cmd.Name.Contains("default"))
             {
                 missingDefault = false;
             }
@@ -317,19 +317,16 @@ public IEnumerable<CompiledFile> GenerateCode(ICompilerConfiguration job, Scope
             {
                 if (proofCmd.Goals.Count == 1 && proofCmd.Goals[0].IsDefault)
                 {
-                    var proof = new ProofCommand("default", null)
-                    {
-                        Goals = [],
-                        Premises = proofCmd.Premises
-                    };
-                    _commands.Add(proof);
-                    _proofCommandToFiles.Add(proof, []);
-                    files.AddRange(CompileToFile($"{filenamePrefix}default", proof, true, true, true));
+                    proofCmd.Name = "default" + proofCmd.Name;
+                    proofCmd.Goals = [];
+                    _commands.Add(proofCmd);
+                    _proofCommandToFiles.Add(proofCmd, []);
+                    files.AddRange(CompileToFile($"{filenamePrefix}default", proofCmd, true, true, true));
                 }
                 else
                 {
                     _proofCommandToFiles.Add(proofCmd, []);
-                    files.AddRange(CompileToFile($"{filenamePrefix}{proofCmd.Name}", proofCmd, true, false, false));
+                    files.AddRange(CompileToFile($"{filenamePrefix}{proofCmd.Name.Replace(",", "_").Replace(" ", "_")}", proofCmd, true, false, false));
                     _commands.Add(proofCmd);
                 }
             }
diff --git a/Src/PCompiler/CompilerCore/TypeChecker/DeclarationStubVisitor.cs b/Src/PCompiler/CompilerCore/TypeChecker/DeclarationStubVisitor.cs
index 34c63233f..704f3b67f 100644
--- a/Src/PCompiler/CompilerCore/TypeChecker/DeclarationStubVisitor.cs
+++ b/Src/PCompiler/CompilerCore/TypeChecker/DeclarationStubVisitor.cs
@@ -61,6 +61,10 @@ public override object VisitInvariantGroupDecl(PParser.InvariantGroupDeclContext
         public override object VisitProveUsingCmd(PParser.ProveUsingCmdContext context)
         {
             var name = string.Join(", ", context._targets.Select(t => t.GetText()));
+            if (context._premises.Count > 0)
+            {
+                name += " using " + string.Join(", ", context._premises.Select(t => t.GetText()));
+            }
             var decl = CurrentScope.Put(name, context);
             nodesToDeclarations.Put(context, decl);
             return null;