Skip to content

Commit

Permalink
copilot-theorem: Look for falsifiable (not invalid). Refs Copilot…
Browse files Browse the repository at this point in the history
…-Language#495.

In Kind2, disproven properties are tagged with `falsifiable` in the XML output,
but the code in `copilot-theorem`'s Kind2 backend was instead searching for a
tag named `invalid`. As a result, `copilot-theorem` would error when attempting
to disprove properties that are false, as it fail to parse the XML output. This
fixes the issue by replacing `invalid` with `falsifiable`.
  • Loading branch information
RyanGlScott committed May 5, 2024
1 parent f823901 commit 866a407
Showing 1 changed file with 3 additions and 3 deletions.
6 changes: 3 additions & 3 deletions copilot-theorem/src/Copilot/Theorem/Kind2/Output.hs
Original file line number Diff line number Diff line change
Expand Up @@ -19,9 +19,9 @@ parseOutput :: String -- ^ Property whose validity is being checked.
parseOutput prop xml = fromJust $ do
root <- parseXMLDoc xml
case findAnswer . findPropTag $ root of
"valid" -> return (Output Valid [])
"invalid" -> return (Output Invalid [])
s -> err $ "Unrecognized status : " ++ s
"valid" -> return (Output Valid [])
"falsifiable" -> return (Output Invalid [])
s -> err $ "Unrecognized status : " ++ s

where

Expand Down

0 comments on commit 866a407

Please sign in to comment.