Skip to content

Commit

Permalink
Reduce DecidePredicateUnknown pretty instance to only rule locations (
Browse files Browse the repository at this point in the history
#3695)

Follow-up for #3694.

Knowing which rule caused `DecidePredicateUnknown` is useful, but seeing
the Kore of the predicate in the logs is not, since we now have it in
the response anyway.
  • Loading branch information
geo2a authored Nov 16, 2023
1 parent b00503f commit 9d751cd
Showing 1 changed file with 2 additions and 22 deletions.
24 changes: 2 additions & 22 deletions kore/src/Kore/Log/DecidePredicateUnknown.hs
Original file line number Diff line number Diff line change
Expand Up @@ -19,7 +19,6 @@ import Control.Exception (
Exception (..),
throw,
)
import Data.Limit (Limit (..))
import Debug
import Kore.Attribute.SourceLocation (
SourceLocation (..),
Expand Down Expand Up @@ -69,27 +68,8 @@ instance Diff DecidePredicateUnknown where
diffPrec = diffPrecEq

instance Pretty DecidePredicateUnknown where
pretty DecidePredicateUnknown{smtLimit = SMT.RetryLimit limit, predicates} =
Pretty.vsep
( [ "Failed to decide predicate:"
, Pretty.indent 4 (pretty predicate)
]
++ do
sideCondition <- sideConditions
[ "with side condition:"
, Pretty.indent 4 (pretty sideCondition)
]
++ [ "SMT limit set at:"
, Pretty.indent
4
( case limit of
Limit n -> pretty n
Unlimited -> "infinity"
)
]
)
where
predicate :| sideConditions = predicates
pretty DecidePredicateUnknown{} =
Pretty.vsep ["Failed to decide predicate."]

instance Entry DecidePredicateUnknown where
entrySeverity DecidePredicateUnknown{action} =
Expand Down

0 comments on commit 9d751cd

Please sign in to comment.