Make Conditional's term a strict field (#2442)

* Make Conditional's term a strict field

* Check if term is bottom before simplify

* Add test

Author: ana-pantilie

kore/src/Kore/Internal/Conditional.hs

@@ -90,7 +90,7 @@ quadratic complexity.
  -}
 data Conditional variable child =
     Conditional
-        { term :: child
+        { term :: !child
         , predicate :: !(Predicate variable)
         , substitution :: !(Substitution variable)
         }

kore/src/Kore/Reachability/Claim.hs

@@ -40,6 +40,7 @@ import Control.Lens
     ( Lens'
     )
 import qualified Control.Lens as Lens
+import qualified Control.Monad as Monad
 import Control.Monad.Catch
     ( Exception (..)
     , SomeException (..)
@@ -604,6 +605,7 @@ simplify' lensClaimPattern claim = do
 
     simplifyLeftHandSide =
         Lens.traverseOf (lensClaimPattern . field @"left") $ \config -> do
+            Monad.guard (not . isBottom . Conditional.term $ config)
             let definedConfig =
                     Pattern.andCondition (mkDefined <$> config)
                     $ from $ makeCeilPredicate (Conditional.term config)

kore/test/Test/Kore/Reachability/Prove.hs

@@ -658,6 +658,21 @@ test_proveClaims =
         [ mkTest "OnePath" simpleOnePathClaim
         , mkTest "AllPath" simpleAllPathClaim
         ]
+    , testGroup "LHS is undefined" $
+        let mkTest name mkSimpleClaim =
+                testCase name $ do
+                    let claims = [mkSimpleClaim mkBottom_ Mock.a]
+                    actual <- proveClaims_
+                        Unlimited
+                        Unlimited
+                        []
+                        claims
+                        []
+                    assertEqual "Result is \\top" MultiAnd.top actual
+        in
+        [ mkTest "OnePath" simpleOnePathClaim
+        , mkTest "AllPath" simpleAllPathClaim
+        ]
     ]
 
 simpleAxiom