From 48eea920c886bd4f51a9b5c9527737f1e95aa51c Mon Sep 17 00:00:00 2001
From: andreiburdusa <andrei.burdusa@zoho.com>
Date: Wed, 29 Jul 2020 14:57:01 +0300
Subject: [PATCH 01/13] Warn when a claim is proven without taking any steps

---
 kore/src/Kore/Log/Registry.hs            |  4 +++
 kore/src/Kore/Log/WarnProvenZeroDepth.hs | 33 ++++++++++++++++++++++++
 kore/src/Kore/Strategies/Verification.hs |  2 ++
 3 files changed, 39 insertions(+)
 create mode 100644 kore/src/Kore/Log/WarnProvenZeroDepth.hs

diff --git a/kore/src/Kore/Log/Registry.hs b/kore/src/Kore/Log/Registry.hs
index c5fb5aa4a0..5206ae9a02 100644
--- a/kore/src/Kore/Log/Registry.hs
+++ b/kore/src/Kore/Log/Registry.hs
@@ -98,6 +98,9 @@ import Kore.Log.WarnFunctionWithoutEvaluators
 import Kore.Log.WarnIfLowProductivity
     ( WarnIfLowProductivity
     )
+import Kore.Log.WarnProvenZeroDepth
+    ( WarnProvenZeroDepth
+    )
 import Kore.Log.WarnStuckProofState
     ( WarnStuckProofState
     )
@@ -152,6 +155,7 @@ entryHelpDocs :: [Pretty.Doc ()]
     , mk $ Proxy @WarnSymbolSMTRepresentation
     , mk $ Proxy @WarnStuckProofState
     , mk $ Proxy @WarnIfLowProductivity
+    , mk $ Proxy @WarnProvenZeroDepth
     , mk $ Proxy @DebugEvaluateCondition
     , mk $ Proxy @ErrorException
     , mk $ Proxy @ErrorRewriteLoop
diff --git a/kore/src/Kore/Log/WarnProvenZeroDepth.hs b/kore/src/Kore/Log/WarnProvenZeroDepth.hs
new file mode 100644
index 0000000000..49d5b3383f
--- /dev/null
+++ b/kore/src/Kore/Log/WarnProvenZeroDepth.hs
@@ -0,0 +1,33 @@
+{- |
+Copyright   : (c) Runtime Verification, 2020
+License     : NCSA
+
+-}
+
+module Kore.Log.WarnProvenZeroDepth
+    ( WarnProvenZeroDepth (..)
+    , warnIfProvenWithZeroDepth
+    ) where
+
+import Prelude.Kore
+
+import Kore.Log.InfoProofDepth
+import Log
+import Pretty
+    ( Pretty
+    )
+import qualified Pretty
+
+data WarnProvenZeroDepth = WarnProvenZeroDepth
+    deriving Show
+
+instance Pretty WarnProvenZeroDepth where
+    pretty _ = "claim proven without taking any steps"
+
+instance Entry WarnProvenZeroDepth where
+    entrySeverity _ = Warning
+    helpDoc _ = "warn when a claim is proven without taking any steps"
+
+warnIfProvenWithZeroDepth :: MonadLog log => ProofDepth -> log ()
+warnIfProvenWithZeroDepth (ProofDepth depth) =
+    when (depth == 0) $ logEntry WarnProvenZeroDepth
diff --git a/kore/src/Kore/Strategies/Verification.hs b/kore/src/Kore/Strategies/Verification.hs
index 35f1c53a62..b0363ddd32 100644
--- a/kore/src/Kore/Strategies/Verification.hs
+++ b/kore/src/Kore/Strategies/Verification.hs
@@ -73,6 +73,7 @@ import qualified Kore.Internal.Pattern as Pattern
 import Kore.Log.DebugProofState
 import Kore.Log.InfoExecBreadth
 import Kore.Log.InfoProofDepth
+import Kore.Log.WarnProvenZeroDepth
 import Kore.Step.RulePattern
     ( leftPattern
     , toRulePattern
@@ -278,6 +279,7 @@ verifyClaim
             & handle handleLimitExceeded
     let maxProofDepth = sconcat (ProofDepth 0 :| proofDepths)
     infoProvenDepth maxProofDepth
+    warnIfProvenWithZeroDepth maxProofDepth
   where
     discardStrategy = snd
 

From 82ca092c0a077dad3b23f18455b18fb3c4347c08 Mon Sep 17 00:00:00 2001
From: andreiburdusa <andrei.burdusa@zoho.com>
Date: Thu, 30 Jul 2020 12:30:46 +0300
Subject: [PATCH 02/13] Warn when trivial claim is removed

---
 kore/src/Kore/Exec.hs                    | 10 ++++---
 kore/src/Kore/Log/Registry.hs            |  8 +++---
 kore/src/Kore/Log/WarnProvenZeroDepth.hs | 33 ------------------------
 kore/src/Kore/Strategies/Verification.hs |  2 +-
 test/tiny/a-to-c-spec.k                  |  2 +-
 5 files changed, 12 insertions(+), 43 deletions(-)
 delete mode 100644 kore/src/Kore/Log/WarnProvenZeroDepth.hs

diff --git a/kore/src/Kore/Exec.hs b/kore/src/Kore/Exec.hs
index e284f90ed7..99bc9bb9ce 100644
--- a/kore/src/Kore/Exec.hs
+++ b/kore/src/Kore/Exec.hs
@@ -103,6 +103,7 @@ import Kore.Log.InfoExecDepth
 import Kore.Log.KoreLogOptions
     ( KoreLogOptions (..)
     )
+import Kore.Log.WarnTrivialClaim
 import qualified Kore.ModelChecker.Bounded as Bounded
 import qualified Kore.Repl as Repl
 import qualified Kore.Repl.Data as Repl.Data
@@ -693,12 +694,13 @@ initializeProver definitionModule specModule maybeTrustedModule = do
         changedSpecClaims =
             expandClaim tools <$> Goal.extractClaims specModule
         simplifyToList
-            :: SimplifyRuleLHS rule
-            => rule
-            -> simplifier [rule]
+            :: ReachabilityRule
+            -> simplifier [ReachabilityRule]
         simplifyToList rule = do
             simplified <- simplifyRuleLhs rule
-            return (MultiAnd.extractPatterns simplified)
+            let result = MultiAnd.extractPatterns simplified
+            when (null result) $ warnTrivialClaimRemoved rule
+            return result
 
         trustedClaims :: [ReachabilityRule]
         trustedClaims =
diff --git a/kore/src/Kore/Log/Registry.hs b/kore/src/Kore/Log/Registry.hs
index 5206ae9a02..31bf46f635 100644
--- a/kore/src/Kore/Log/Registry.hs
+++ b/kore/src/Kore/Log/Registry.hs
@@ -98,15 +98,15 @@ import Kore.Log.WarnFunctionWithoutEvaluators
 import Kore.Log.WarnIfLowProductivity
     ( WarnIfLowProductivity
     )
-import Kore.Log.WarnProvenZeroDepth
-    ( WarnProvenZeroDepth
-    )
 import Kore.Log.WarnStuckProofState
     ( WarnStuckProofState
     )
 import Kore.Log.WarnSymbolSMTRepresentation
     ( WarnSymbolSMTRepresentation
     )
+import Kore.Log.WarnTrivialClaim
+    ( WarnTrivialClaim
+    )
 import Log
     ( Entry (..)
     , LogMessage
@@ -155,7 +155,7 @@ entryHelpDocs :: [Pretty.Doc ()]
     , mk $ Proxy @WarnSymbolSMTRepresentation
     , mk $ Proxy @WarnStuckProofState
     , mk $ Proxy @WarnIfLowProductivity
-    , mk $ Proxy @WarnProvenZeroDepth
+    , mk $ Proxy @WarnTrivialClaim
     , mk $ Proxy @DebugEvaluateCondition
     , mk $ Proxy @ErrorException
     , mk $ Proxy @ErrorRewriteLoop
diff --git a/kore/src/Kore/Log/WarnProvenZeroDepth.hs b/kore/src/Kore/Log/WarnProvenZeroDepth.hs
deleted file mode 100644
index 49d5b3383f..0000000000
--- a/kore/src/Kore/Log/WarnProvenZeroDepth.hs
+++ /dev/null
@@ -1,33 +0,0 @@
-{- |
-Copyright   : (c) Runtime Verification, 2020
-License     : NCSA
-
--}
-
-module Kore.Log.WarnProvenZeroDepth
-    ( WarnProvenZeroDepth (..)
-    , warnIfProvenWithZeroDepth
-    ) where
-
-import Prelude.Kore
-
-import Kore.Log.InfoProofDepth
-import Log
-import Pretty
-    ( Pretty
-    )
-import qualified Pretty
-
-data WarnProvenZeroDepth = WarnProvenZeroDepth
-    deriving Show
-
-instance Pretty WarnProvenZeroDepth where
-    pretty _ = "claim proven without taking any steps"
-
-instance Entry WarnProvenZeroDepth where
-    entrySeverity _ = Warning
-    helpDoc _ = "warn when a claim is proven without taking any steps"
-
-warnIfProvenWithZeroDepth :: MonadLog log => ProofDepth -> log ()
-warnIfProvenWithZeroDepth (ProofDepth depth) =
-    when (depth == 0) $ logEntry WarnProvenZeroDepth
diff --git a/kore/src/Kore/Strategies/Verification.hs b/kore/src/Kore/Strategies/Verification.hs
index b0363ddd32..3fe806aa7e 100644
--- a/kore/src/Kore/Strategies/Verification.hs
+++ b/kore/src/Kore/Strategies/Verification.hs
@@ -73,7 +73,7 @@ import qualified Kore.Internal.Pattern as Pattern
 import Kore.Log.DebugProofState
 import Kore.Log.InfoExecBreadth
 import Kore.Log.InfoProofDepth
-import Kore.Log.WarnProvenZeroDepth
+import Kore.Log.WarnTrivialClaim
 import Kore.Step.RulePattern
     ( leftPattern
     , toRulePattern
diff --git a/test/tiny/a-to-c-spec.k b/test/tiny/a-to-c-spec.k
index b1d82eccfe..760b769de3 100644
--- a/test/tiny/a-to-c-spec.k
+++ b/test/tiny/a-to-c-spec.k
@@ -6,6 +6,6 @@ endmodule
 module A-TO-C-SPEC
   imports VERIFICATION
 
-  rule a => c
+  rule a #And b => c
 
 endmodule

From f57f9f1ce22d8bbb03942446a9a9eb4da5d2fc63 Mon Sep 17 00:00:00 2001
From: andreiburdusa <andrei.burdusa@zoho.com>
Date: Thu, 30 Jul 2020 13:55:57 +0300
Subject: [PATCH 03/13] Location is Nothing

---
 kore/src/Kore/Exec.hs                 |  7 +++-
 kore/src/Kore/Log/WarnTrivialClaim.hs | 58 +++++++++++++++++++++++++++
 test/tiny/a-to-c-spec.k               |  2 +-
 3 files changed, 65 insertions(+), 2 deletions(-)
 create mode 100644 kore/src/Kore/Log/WarnTrivialClaim.hs

diff --git a/kore/src/Kore/Exec.hs b/kore/src/Kore/Exec.hs
index 99bc9bb9ce..0ec2c7d854 100644
--- a/kore/src/Kore/Exec.hs
+++ b/kore/src/Kore/Exec.hs
@@ -66,7 +66,8 @@ import Kore.Equation
     ( Equation
     )
 import Kore.IndexedModule.IndexedModule
-    ( VerifiedModule
+    ( IndexedModule (..)
+    , VerifiedModule
     )
 import qualified Kore.IndexedModule.IndexedModule as IndexedModule
 import Kore.IndexedModule.MetadataTools
@@ -687,6 +688,10 @@ initializeProver
     -> Maybe (VerifiedModule StepperAttributes)
     -> simplifier InitializedProver
 initializeProver definitionModule specModule maybeTrustedModule = do
+    traceM $
+        "\nLoc"
+        <> (show . Attribute.sourceLocation . fst . head . indexedModuleClaims)
+            specModule
     initialized <- initialize definitionModule
     tools <- Simplifier.askMetadataTools
     let Initialized { rewriteRules } = initialized
diff --git a/kore/src/Kore/Log/WarnTrivialClaim.hs b/kore/src/Kore/Log/WarnTrivialClaim.hs
new file mode 100644
index 0000000000..dc6152d806
--- /dev/null
+++ b/kore/src/Kore/Log/WarnTrivialClaim.hs
@@ -0,0 +1,58 @@
+{- |
+Copyright   : (c) Runtime Verification, 2020
+License     : NCSA
+
+-}
+
+module Kore.Log.WarnTrivialClaim
+    ( WarnTrivialClaim (..)
+    , warnIfProvenWithZeroDepth
+    , warnTrivialClaimRemoved
+    ) where
+
+import Prelude.Kore
+
+import Kore.Attribute.SourceLocation
+import Kore.Log.InfoProofDepth
+import Kore.Step.RulePattern
+import Log
+import Pretty
+    ( Pretty
+    )
+import qualified Pretty
+
+data WarnTrivialClaim
+    = WarnProvenClaimZeroDepth
+    | WarnTrivialClaimRemoved ReachabilityRule
+    deriving Show
+
+instance Pretty WarnTrivialClaim where
+    pretty WarnProvenClaimZeroDepth =
+        Pretty.hsep
+            [ "claim proven without taking any steps:"
+            ]
+    pretty (WarnTrivialClaimRemoved rule) =
+        Pretty.hsep
+            [ "trivial claim removed:"
+            , Pretty.pretty $ show (from rule :: SourceLocation)
+            ]
+
+
+instance Entry WarnTrivialClaim where
+    entrySeverity _ = Warning
+    helpDoc _ =
+        "warn when a claim is removed or proven without taking any steps"
+
+warnIfProvenWithZeroDepth
+    :: MonadLog log
+    => ProofDepth
+    -> log ()
+warnIfProvenWithZeroDepth (ProofDepth depth) =
+    when (depth == 0) $ logEntry WarnProvenClaimZeroDepth
+
+warnTrivialClaimRemoved
+    :: MonadLog log
+    => ReachabilityRule
+    -> log ()
+warnTrivialClaimRemoved rule =
+    logEntry (WarnTrivialClaimRemoved rule)
diff --git a/test/tiny/a-to-c-spec.k b/test/tiny/a-to-c-spec.k
index 760b769de3..b1d82eccfe 100644
--- a/test/tiny/a-to-c-spec.k
+++ b/test/tiny/a-to-c-spec.k
@@ -6,6 +6,6 @@ endmodule
 module A-TO-C-SPEC
   imports VERIFICATION
 
-  rule a #And b => c
+  rule a => c
 
 endmodule

From 871103b9ad9c83082ad6b733cdc03ea33015b8cf Mon Sep 17 00:00:00 2001
From: andreiburdusa <andrei.burdusa@zoho.com>
Date: Thu, 30 Jul 2020 17:26:53 +0300
Subject: [PATCH 04/13] Debug

---
 kore/app/exec/Main.hs               | 13 ++++++++++++-
 kore/src/Kore/Attribute/Location.hs |  1 +
 kore/src/Kore/Exec.hs               |  6 +++---
 3 files changed, 16 insertions(+), 4 deletions(-)

diff --git a/kore/app/exec/Main.hs b/kore/app/exec/Main.hs
index c0aaa6d1d5..fd159442c5 100644
--- a/kore/app/exec/Main.hs
+++ b/kore/app/exec/Main.hs
@@ -86,6 +86,7 @@ import Kore.Exec
 import Kore.IndexedModule.IndexedModule
     ( VerifiedModule
     , indexedModuleRawSentences
+    , IndexedModule (..)
     )
 import qualified Kore.IndexedModule.MetadataToolsBuilder as MetadataTools
     ( build
@@ -98,6 +99,7 @@ import Kore.Internal.Pattern
 import Kore.Internal.Predicate
     ( makePredicate
     )
+import qualified Kore.Attribute.Axiom as Attribute.Axiom
 import Kore.Internal.TermLike
     ( pattern And_
     , TermLike
@@ -663,12 +665,21 @@ koreProve execOptions proveOptions = do
     mainModule <- loadModule mainModuleName definition
     let KoreProveOptions { specMainModule } = proveOptions
     specModule <- loadModule specMainModule definition
+    traceM $
+        "\nLoc koreProve: "
+        <>  ( show
+            . Attribute.Axiom.sourceLocation
+            . fst
+            . head
+            . indexedModuleClaims
+            )
+            specModule
     let KoreProveOptions { saveProofs } = proveOptions
     maybeAlreadyProvenModule <- loadProven definitionFileName saveProofs
     proveResult <- execute execOptions mainModule $ do
         let KoreExecOptions { breadthLimit, depthLimit } = execOptions
             KoreProveOptions { graphSearch } = proveOptions
-        prove
+        proveQ
             graphSearch
             breadthLimit
             depthLimit
diff --git a/kore/src/Kore/Attribute/Location.hs b/kore/src/Kore/Attribute/Location.hs
index 930af7c2b8..cf0084d9dd 100644
--- a/kore/src/Kore/Attribute/Location.hs
+++ b/kore/src/Kore/Attribute/Location.hs
@@ -81,6 +81,7 @@ instance ParseAttributes Location where
                 [_] -> do
                     arg <- AttributeParser.getOneArgument args
                     StringLiteral str <- AttributeParser.getStringLiteral arg
+                    traceM $ "STR to be parsed " <> Text.unpack str
                     pure
                         . fromMaybe def
                         . parseMaybe locationParser
diff --git a/kore/src/Kore/Exec.hs b/kore/src/Kore/Exec.hs
index 0ec2c7d854..c516bcb311 100644
--- a/kore/src/Kore/Exec.hs
+++ b/kore/src/Kore/Exec.hs
@@ -14,7 +14,7 @@ module Kore.Exec
     , mergeAllRules
     , mergeRulesConsecutiveBatches
     , search
-    , prove
+    , proveQ
     , proveWithRepl
     , boundedModelCheck
     , Rewrite
@@ -356,7 +356,7 @@ search breadthLimit verifiedModule strategy termLike searchPattern searchConfig
 
 
 -- | Proving a spec given as a module containing rules to be proven
-prove
+proveQ
     ::  forall smt
       . ( MonadLog smt
         , MonadMask smt
@@ -374,7 +374,7 @@ prove
     -> Maybe (VerifiedModule StepperAttributes)
     -- ^ The module containing the claims that were proven in a previous run.
     -> smt (Either Stuck ())
-prove
+proveQ
     searchOrder
     breadthLimit
     depthLimit

From b5a5627530d9f3eea3a58a1a3b60afc71e078776 Mon Sep 17 00:00:00 2001
From: andreiburdusa <andrei.burdusa@zoho.com>
Date: Tue, 4 Aug 2020 10:04:06 +0300
Subject: [PATCH 05/13] Trace

---
 kore/app/exec/Main.hs               | 14 +++++---------
 kore/src/Kore/Attribute/Location.hs |  1 -
 kore/src/Kore/Exec.hs               |  4 ----
 test/tiny/a-to-c-spec.k             |  2 +-
 4 files changed, 6 insertions(+), 15 deletions(-)

diff --git a/kore/app/exec/Main.hs b/kore/app/exec/Main.hs
index fd159442c5..359ce898f5 100644
--- a/kore/app/exec/Main.hs
+++ b/kore/app/exec/Main.hs
@@ -660,20 +660,16 @@ koreProve :: KoreExecOptions -> KoreProveOptions -> Main ExitCode
 koreProve execOptions proveOptions = do
     let KoreExecOptions { definitionFileName } = execOptions
         KoreProveOptions { specFileName } = proveOptions
+    traceM $ "Spec File Name: " <> specFileName
     definition <- loadDefinitions [definitionFileName, specFileName]
+    traceM $ show $
+        fmap (fmap (Attribute.Axiom.sourceLocation . fst). indexedModuleClaims)
+        . fst
+        $ definition
     let KoreExecOptions { mainModuleName } = execOptions
     mainModule <- loadModule mainModuleName definition
     let KoreProveOptions { specMainModule } = proveOptions
     specModule <- loadModule specMainModule definition
-    traceM $
-        "\nLoc koreProve: "
-        <>  ( show
-            . Attribute.Axiom.sourceLocation
-            . fst
-            . head
-            . indexedModuleClaims
-            )
-            specModule
     let KoreProveOptions { saveProofs } = proveOptions
     maybeAlreadyProvenModule <- loadProven definitionFileName saveProofs
     proveResult <- execute execOptions mainModule $ do
diff --git a/kore/src/Kore/Attribute/Location.hs b/kore/src/Kore/Attribute/Location.hs
index cf0084d9dd..930af7c2b8 100644
--- a/kore/src/Kore/Attribute/Location.hs
+++ b/kore/src/Kore/Attribute/Location.hs
@@ -81,7 +81,6 @@ instance ParseAttributes Location where
                 [_] -> do
                     arg <- AttributeParser.getOneArgument args
                     StringLiteral str <- AttributeParser.getStringLiteral arg
-                    traceM $ "STR to be parsed " <> Text.unpack str
                     pure
                         . fromMaybe def
                         . parseMaybe locationParser
diff --git a/kore/src/Kore/Exec.hs b/kore/src/Kore/Exec.hs
index c516bcb311..02afa42975 100644
--- a/kore/src/Kore/Exec.hs
+++ b/kore/src/Kore/Exec.hs
@@ -688,10 +688,6 @@ initializeProver
     -> Maybe (VerifiedModule StepperAttributes)
     -> simplifier InitializedProver
 initializeProver definitionModule specModule maybeTrustedModule = do
-    traceM $
-        "\nLoc"
-        <> (show . Attribute.sourceLocation . fst . head . indexedModuleClaims)
-            specModule
     initialized <- initialize definitionModule
     tools <- Simplifier.askMetadataTools
     let Initialized { rewriteRules } = initialized
diff --git a/test/tiny/a-to-c-spec.k b/test/tiny/a-to-c-spec.k
index b1d82eccfe..760b769de3 100644
--- a/test/tiny/a-to-c-spec.k
+++ b/test/tiny/a-to-c-spec.k
@@ -6,6 +6,6 @@ endmodule
 module A-TO-C-SPEC
   imports VERIFICATION
 
-  rule a => c
+  rule a #And b => c
 
 endmodule

From 8f27ffa0b46b874ca0d9878e4c970b6c6f3df136 Mon Sep 17 00:00:00 2001
From: andreiburdusa <andrei.burdusa@zoho.com>
Date: Wed, 5 Aug 2020 13:46:09 +0300
Subject: [PATCH 06/13] trace

---
 kore/app/exec/Main.hs | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/kore/app/exec/Main.hs b/kore/app/exec/Main.hs
index 359ce898f5..55523b0083 100644
--- a/kore/app/exec/Main.hs
+++ b/kore/app/exec/Main.hs
@@ -80,6 +80,7 @@ import System.IO
     )
 
 import qualified Data.Limit as Limit
+import qualified Data.Map.Strict as Map
 import Kore.Attribute.Symbol as Attribute
 import Kore.BugReport
 import Kore.Exec
@@ -660,11 +661,10 @@ koreProve :: KoreExecOptions -> KoreProveOptions -> Main ExitCode
 koreProve execOptions proveOptions = do
     let KoreExecOptions { definitionFileName } = execOptions
         KoreProveOptions { specFileName } = proveOptions
-    traceM $ "Spec File Name: " <> specFileName
     definition <- loadDefinitions [definitionFileName, specFileName]
     traceM $ show $
         fmap (fmap (Attribute.Axiom.sourceLocation . fst). indexedModuleClaims)
-        . fst
+        . Map.elems . fst
         $ definition
     let KoreExecOptions { mainModuleName } = execOptions
     mainModule <- loadModule mainModuleName definition

From 3661a6fc167e9775cd71c1f5beac29c23825fa8a Mon Sep 17 00:00:00 2001
From: andreiburdusa <andrei.burdusa@zoho.com>
Date: Wed, 5 Aug 2020 16:30:32 +0300
Subject: [PATCH 07/13] Remove traceM

---
 kore/app/exec/Main.hs | 4 ----
 1 file changed, 4 deletions(-)

diff --git a/kore/app/exec/Main.hs b/kore/app/exec/Main.hs
index 55523b0083..4ec63ca4c6 100644
--- a/kore/app/exec/Main.hs
+++ b/kore/app/exec/Main.hs
@@ -662,10 +662,6 @@ koreProve execOptions proveOptions = do
     let KoreExecOptions { definitionFileName } = execOptions
         KoreProveOptions { specFileName } = proveOptions
     definition <- loadDefinitions [definitionFileName, specFileName]
-    traceM $ show $
-        fmap (fmap (Attribute.Axiom.sourceLocation . fst). indexedModuleClaims)
-        . Map.elems . fst
-        $ definition
     let KoreExecOptions { mainModuleName } = execOptions
     mainModule <- loadModule mainModuleName definition
     let KoreProveOptions { specMainModule } = proveOptions

From 3b193a77929c8095688dfc8ee06f3e76030dde92 Mon Sep 17 00:00:00 2001
From: andreiburdusa <andrei.burdusa@zoho.com>
Date: Wed, 5 Aug 2020 16:37:29 +0300
Subject: [PATCH 08/13] cleanup

---
 kore/app/exec/Main.hs | 3 ---
 kore/src/Kore/Exec.hs | 3 +--
 2 files changed, 1 insertion(+), 5 deletions(-)

diff --git a/kore/app/exec/Main.hs b/kore/app/exec/Main.hs
index 4ec63ca4c6..3df0ef1929 100644
--- a/kore/app/exec/Main.hs
+++ b/kore/app/exec/Main.hs
@@ -80,14 +80,12 @@ import System.IO
     )
 
 import qualified Data.Limit as Limit
-import qualified Data.Map.Strict as Map
 import Kore.Attribute.Symbol as Attribute
 import Kore.BugReport
 import Kore.Exec
 import Kore.IndexedModule.IndexedModule
     ( VerifiedModule
     , indexedModuleRawSentences
-    , IndexedModule (..)
     )
 import qualified Kore.IndexedModule.MetadataToolsBuilder as MetadataTools
     ( build
@@ -100,7 +98,6 @@ import Kore.Internal.Pattern
 import Kore.Internal.Predicate
     ( makePredicate
     )
-import qualified Kore.Attribute.Axiom as Attribute.Axiom
 import Kore.Internal.TermLike
     ( pattern And_
     , TermLike
diff --git a/kore/src/Kore/Exec.hs b/kore/src/Kore/Exec.hs
index 02afa42975..21f0fb1dce 100644
--- a/kore/src/Kore/Exec.hs
+++ b/kore/src/Kore/Exec.hs
@@ -66,8 +66,7 @@ import Kore.Equation
     ( Equation
     )
 import Kore.IndexedModule.IndexedModule
-    ( IndexedModule (..)
-    , VerifiedModule
+    ( VerifiedModule
     )
 import qualified Kore.IndexedModule.IndexedModule as IndexedModule
 import Kore.IndexedModule.MetadataTools

From 7fd4f049b6be3c5f397c101c0b43db60cb692360 Mon Sep 17 00:00:00 2001
From: andreiburdusa <andrei.burdusa@zoho.com>
Date: Wed, 5 Aug 2020 16:39:45 +0300
Subject: [PATCH 09/13] Revert more changes used for debugging

---
 kore/app/exec/Main.hs   | 2 +-
 kore/src/Kore/Exec.hs   | 6 +++---
 test/tiny/a-to-c-spec.k | 2 +-
 3 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/kore/app/exec/Main.hs b/kore/app/exec/Main.hs
index 3df0ef1929..c0aaa6d1d5 100644
--- a/kore/app/exec/Main.hs
+++ b/kore/app/exec/Main.hs
@@ -668,7 +668,7 @@ koreProve execOptions proveOptions = do
     proveResult <- execute execOptions mainModule $ do
         let KoreExecOptions { breadthLimit, depthLimit } = execOptions
             KoreProveOptions { graphSearch } = proveOptions
-        proveQ
+        prove
             graphSearch
             breadthLimit
             depthLimit
diff --git a/kore/src/Kore/Exec.hs b/kore/src/Kore/Exec.hs
index 21f0fb1dce..99bc9bb9ce 100644
--- a/kore/src/Kore/Exec.hs
+++ b/kore/src/Kore/Exec.hs
@@ -14,7 +14,7 @@ module Kore.Exec
     , mergeAllRules
     , mergeRulesConsecutiveBatches
     , search
-    , proveQ
+    , prove
     , proveWithRepl
     , boundedModelCheck
     , Rewrite
@@ -355,7 +355,7 @@ search breadthLimit verifiedModule strategy termLike searchPattern searchConfig
 
 
 -- | Proving a spec given as a module containing rules to be proven
-proveQ
+prove
     ::  forall smt
       . ( MonadLog smt
         , MonadMask smt
@@ -373,7 +373,7 @@ proveQ
     -> Maybe (VerifiedModule StepperAttributes)
     -- ^ The module containing the claims that were proven in a previous run.
     -> smt (Either Stuck ())
-proveQ
+prove
     searchOrder
     breadthLimit
     depthLimit
diff --git a/test/tiny/a-to-c-spec.k b/test/tiny/a-to-c-spec.k
index 760b769de3..b1d82eccfe 100644
--- a/test/tiny/a-to-c-spec.k
+++ b/test/tiny/a-to-c-spec.k
@@ -6,6 +6,6 @@ endmodule
 module A-TO-C-SPEC
   imports VERIFICATION
 
-  rule a #And b => c
+  rule a => c
 
 endmodule

From a30dae55eeefc132bee6fb34adb6d6ee2112590e Mon Sep 17 00:00:00 2001
From: andreiburdusa <andrei.burdusa@zoho.com>
Date: Thu, 6 Aug 2020 17:44:37 +0300
Subject: [PATCH 10/13] Pretty print location

---
 kore/src/Kore/Log/WarnTrivialClaim.hs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/kore/src/Kore/Log/WarnTrivialClaim.hs b/kore/src/Kore/Log/WarnTrivialClaim.hs
index dc6152d806..a2edd6956e 100644
--- a/kore/src/Kore/Log/WarnTrivialClaim.hs
+++ b/kore/src/Kore/Log/WarnTrivialClaim.hs
@@ -34,7 +34,7 @@ instance Pretty WarnTrivialClaim where
     pretty (WarnTrivialClaimRemoved rule) =
         Pretty.hsep
             [ "trivial claim removed:"
-            , Pretty.pretty $ show (from rule :: SourceLocation)
+            , Pretty.pretty (from rule :: SourceLocation)
             ]
 
 

From 67ae4a8c51ac413a88a397890d45a1e87e382070 Mon Sep 17 00:00:00 2001
From: andreiburdusa <andrei.burdusa@zoho.com>
Date: Mon, 10 Aug 2020 12:41:07 +0300
Subject: [PATCH 11/13] Print location when depth is 0

---
 kore/src/Kore/Log/WarnTrivialClaim.hs    | 10 ++++++----
 kore/src/Kore/Strategies/Verification.hs |  2 +-
 2 files changed, 7 insertions(+), 5 deletions(-)

diff --git a/kore/src/Kore/Log/WarnTrivialClaim.hs b/kore/src/Kore/Log/WarnTrivialClaim.hs
index a2edd6956e..46558edff6 100644
--- a/kore/src/Kore/Log/WarnTrivialClaim.hs
+++ b/kore/src/Kore/Log/WarnTrivialClaim.hs
@@ -22,14 +22,15 @@ import Pretty
 import qualified Pretty
 
 data WarnTrivialClaim
-    = WarnProvenClaimZeroDepth
+    = WarnProvenClaimZeroDepth ReachabilityRule
     | WarnTrivialClaimRemoved ReachabilityRule
     deriving Show
 
 instance Pretty WarnTrivialClaim where
-    pretty WarnProvenClaimZeroDepth =
+    pretty (WarnProvenClaimZeroDepth rule) =
         Pretty.hsep
             [ "claim proven without taking any steps:"
+            , Pretty.pretty (from rule :: SourceLocation)
             ]
     pretty (WarnTrivialClaimRemoved rule) =
         Pretty.hsep
@@ -46,9 +47,10 @@ instance Entry WarnTrivialClaim where
 warnIfProvenWithZeroDepth
     :: MonadLog log
     => ProofDepth
+    -> ReachabilityRule
     -> log ()
-warnIfProvenWithZeroDepth (ProofDepth depth) =
-    when (depth == 0) $ logEntry WarnProvenClaimZeroDepth
+warnIfProvenWithZeroDepth (ProofDepth depth) rule =
+    when (depth == 0) $ logEntry (WarnProvenClaimZeroDepth rule)
 
 warnTrivialClaimRemoved
     :: MonadLog log
diff --git a/kore/src/Kore/Strategies/Verification.hs b/kore/src/Kore/Strategies/Verification.hs
index c69c0fb583..27c703d630 100644
--- a/kore/src/Kore/Strategies/Verification.hs
+++ b/kore/src/Kore/Strategies/Verification.hs
@@ -279,7 +279,7 @@ verifyClaim
             & handle handleLimitExceeded
     let maxProofDepth = sconcat (ProofDepth 0 :| proofDepths)
     infoProvenDepth maxProofDepth
-    warnIfProvenWithZeroDepth maxProofDepth
+    warnIfProvenWithZeroDepth maxProofDepth goal
   where
     discardStrategy = snd
 

From 5369c1ebe3a610262dd88f528c3551541518be3b Mon Sep 17 00:00:00 2001
From: Thomas Tuegel <thomas.tuegel@runtimeverification.com>
Date: Mon, 10 Aug 2020 10:36:56 -0500
Subject: [PATCH 12/13] warnProvenClaimZeroDepth: Match function name to
 constructor name

---
 kore/src/Kore/Log/WarnTrivialClaim.hs    | 6 +++---
 kore/src/Kore/Strategies/Verification.hs | 2 +-
 2 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/kore/src/Kore/Log/WarnTrivialClaim.hs b/kore/src/Kore/Log/WarnTrivialClaim.hs
index 46558edff6..a9783f7c3e 100644
--- a/kore/src/Kore/Log/WarnTrivialClaim.hs
+++ b/kore/src/Kore/Log/WarnTrivialClaim.hs
@@ -6,7 +6,7 @@ License     : NCSA
 
 module Kore.Log.WarnTrivialClaim
     ( WarnTrivialClaim (..)
-    , warnIfProvenWithZeroDepth
+    , warnProvenClaimZeroDepth
     , warnTrivialClaimRemoved
     ) where
 
@@ -44,12 +44,12 @@ instance Entry WarnTrivialClaim where
     helpDoc _ =
         "warn when a claim is removed or proven without taking any steps"
 
-warnIfProvenWithZeroDepth
+warnProvenClaimZeroDepth
     :: MonadLog log
     => ProofDepth
     -> ReachabilityRule
     -> log ()
-warnIfProvenWithZeroDepth (ProofDepth depth) rule =
+warnProvenClaimZeroDepth (ProofDepth depth) rule =
     when (depth == 0) $ logEntry (WarnProvenClaimZeroDepth rule)
 
 warnTrivialClaimRemoved
diff --git a/kore/src/Kore/Strategies/Verification.hs b/kore/src/Kore/Strategies/Verification.hs
index 27c703d630..ff63216a9f 100644
--- a/kore/src/Kore/Strategies/Verification.hs
+++ b/kore/src/Kore/Strategies/Verification.hs
@@ -279,7 +279,7 @@ verifyClaim
             & handle handleLimitExceeded
     let maxProofDepth = sconcat (ProofDepth 0 :| proofDepths)
     infoProvenDepth maxProofDepth
-    warnIfProvenWithZeroDepth maxProofDepth goal
+    warnProvenClaimZeroDepth maxProofDepth goal
   where
     discardStrategy = snd
 

From 1e57f4150ce6f46ff18477421e6d43c24c9f297c Mon Sep 17 00:00:00 2001
From: Thomas Tuegel <thomas.tuegel@runtimeverification.com>
Date: Mon, 10 Aug 2020 10:37:09 -0500
Subject: [PATCH 13/13] Kore.Log.WarnTrivialClaim: Documentation

---
 kore/src/Kore/Log/WarnTrivialClaim.hs | 16 ++++++++++------
 1 file changed, 10 insertions(+), 6 deletions(-)

diff --git a/kore/src/Kore/Log/WarnTrivialClaim.hs b/kore/src/Kore/Log/WarnTrivialClaim.hs
index a9783f7c3e..ee5e22df87 100644
--- a/kore/src/Kore/Log/WarnTrivialClaim.hs
+++ b/kore/src/Kore/Log/WarnTrivialClaim.hs
@@ -23,26 +23,30 @@ import qualified Pretty
 
 data WarnTrivialClaim
     = WarnProvenClaimZeroDepth ReachabilityRule
+    -- ^ Warning when a claim is proved without rewriting.
     | WarnTrivialClaimRemoved ReachabilityRule
+    -- ^ Warning when a claim is proved during initialization.
     deriving Show
 
 instance Pretty WarnTrivialClaim where
     pretty (WarnProvenClaimZeroDepth rule) =
         Pretty.hsep
-            [ "claim proven without taking any steps:"
+            [ "Claim proven without rewriting at:"
             , Pretty.pretty (from rule :: SourceLocation)
             ]
     pretty (WarnTrivialClaimRemoved rule) =
-        Pretty.hsep
-            [ "trivial claim removed:"
-            , Pretty.pretty (from rule :: SourceLocation)
+        Pretty.vsep
+            [ Pretty.hsep
+                [ "Claim proven during initialization:"
+                , Pretty.pretty (from rule :: SourceLocation)
+                ]
+            , "The left-hand side of the claim may be undefined."
             ]
 
 
 instance Entry WarnTrivialClaim where
     entrySeverity _ = Warning
-    helpDoc _ =
-        "warn when a claim is removed or proven without taking any steps"
+    helpDoc _ = "warn when a claim is proven without taking any steps"
 
 warnProvenClaimZeroDepth
     :: MonadLog log