From 866a40769ab3c5f2103fceb93f2c1b390e9db979 Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Mon, 22 Apr 2024 08:58:46 -0400 Subject: [PATCH] copilot-theorem: Look for `falsifiable` (not `invalid`). Refs #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`. --- copilot-theorem/src/Copilot/Theorem/Kind2/Output.hs | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/copilot-theorem/src/Copilot/Theorem/Kind2/Output.hs b/copilot-theorem/src/Copilot/Theorem/Kind2/Output.hs index 49da4790..42a2f60d 100644 --- a/copilot-theorem/src/Copilot/Theorem/Kind2/Output.hs +++ b/copilot-theorem/src/Copilot/Theorem/Kind2/Output.hs @@ -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