add EnsuresFalse case to simplify endpoint, WIP cases for tracing

runtimeverification · Jul 11, 2023 · 3b8806a · 3b8806a
1 parent c002568
commit 3b8806a
Showing 1 changed file with 14 additions and 0 deletions.
diff --git a/library/Booster/JsonRpc.hs b/library/Booster/JsonRpc.hs
@@ -153,6 +153,13 @@ respond stateVar =
                                     { state = addHeader result
                                     , logs = mkTraces patternTraces
                                     }
+                        Left (ApplyEquations.SideConditionsFalse _) -> do
+                            let tSort = fromMaybe (error "unknown sort") $ sortOfJson req.state.term
+                            pure . Right . Simplify $
+                                SimplifyResult
+                                    { state = addHeader $ KoreJson.KJBottom tSort
+                                    , logs = mkTraces [] -- FIXME add traces
+                                    }
                         Left (ApplyEquations.EquationLoop _traces terms) ->
                             pure . Left . backendError RpcError.Aborted $ map externaliseTerm terms -- FIXME
                         Left other ->
@@ -509,4 +516,11 @@ mkLogRewriteTrace
                                     , origin = Booster
                                     , result = Failure{reason = "Internal error: " <> err, _ruleId = Nothing}
                                     }
+                            ApplyEquations.SideConditionsFalse{} ->
+                                Simplification -- FIXME
+                                    { originalTerm = Nothing
+                                    , originalTermIndex = Nothing
+                                    , origin = Booster
+                                    , result = Failure{reason = "Side conditions false", _ruleId = Nothing}
+                                    }
             _ -> Nothing