Skip to content

Commit 226a108

Browse files
committed
copilot-theorem: Look for falsifiable (not invalid). Refs Copilot-Language#495.
In Kind2-0.7.2, 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`.
1 parent db60ae7 commit 226a108

File tree

1 file changed

+1
-1
lines changed
  • copilot-theorem/src/Copilot/Theorem/Kind2

1 file changed

+1
-1
lines changed

copilot-theorem/src/Copilot/Theorem/Kind2/Output.hs

+1-1
Original file line numberDiff line numberDiff line change
@@ -20,7 +20,7 @@ parseOutput prop xml = fromJust $ do
2020
root <- parseXMLDoc xml
2121
case findAnswer . findPropTag $ root of
2222
"valid" -> return (Output Valid [])
23-
"invalid" -> return (Output Invalid [])
23+
"falsifiable" -> return (Output Invalid [])
2424
s -> err $ "Unrecognized status : " ++ s
2525

2626
where

0 commit comments

Comments
 (0)