diff --git a/booster/library/Booster/Pattern/Implies.hs b/booster/library/Booster/Pattern/Implies.hs index e1d115f328..bf521a00e0 100644 --- a/booster/library/Booster/Pattern/Implies.hs +++ b/booster/library/Booster/Pattern/Implies.hs @@ -137,32 +137,68 @@ runImplies def mLlvmLibrary mSMTOptions antecedent consequent = (Left err, _) -> pure . Left . RpcError.backendError $ RpcError.Aborted (Text.pack . constructorName $ err) MatchSuccess subst -> do - let filteredConsequentPreds = - (patR.constraints <> (Set.fromList $ asEquations patR.substitution)) - `Set.difference` (patL.constraints <> (Set.fromList $ asEquations patL.substitution)) - + let sort = sortOfPattern patL + lhs = externaliseExistTerm existsL patL.term + rhs = externaliseExistTerm existsR patR.term + antecedentPreds = + patL.constraints <> Set.fromList (asEquations patL.substitution) + filteredConsequentPreds = + (patR.constraints <> Set.fromList (asEquations patR.substitution)) + `Set.difference` antecedentPreds if null filteredConsequentPreds - then - implies - (sortOfPattern patL) - (externaliseExistTerm existsL patL.term) - (externaliseExistTerm existsR patR.term) - subst - else -- FIXME This is incomplete because patL.constraints are not assumed in the check. - - ApplyEquations.evaluateConstraints def mLlvmLibrary solver filteredConsequentPreds >>= \case - Right newPreds -> - if all (== Predicate TrueBool) newPreds - then - implies - (sortOfPattern patL) - (externaliseExistTerm existsL patL.term) - (externaliseExistTerm existsR patR.term) - subst - else -- here we conservatively abort (incomplete) - pure . Left . RpcError.backendError $ RpcError.Aborted "unknown constraints" - Left other -> - pure . Left . RpcError.backendError $ RpcError.Aborted (Text.pack . constructorName $ other) + then implies sort lhs rhs subst + else do + -- Discharge the leftover consequent obligations under + -- the antecedent. Two stages: + -- 1. Simplify each obligation with the antecedent in + -- 'knownPredicates' so function-symbol unfolds + -- (e.g. '#rangeAddress') and boolean structure + -- collapse can fire. + -- 2. SMT-close any non-'TrueBool' residue against + -- 'antecedentPreds' / 'patL.substitution' — the + -- same pattern the rewrite path uses to discharge + -- rule requires-clauses + -- ('Booster.Pattern.Rewrite.checkRequires'). + simplified <- + mapM + ( fmap fst + . ApplyEquations.simplifyConstraint + def + mLlvmLibrary + solver + mempty + antecedentPreds + ) + (Set.toList filteredConsequentPreds) + let impliesResult = implies sort lhs rhs subst + unsure = doesNotImplyIndeterminate sort lhs rhs + disjoint = doesNotImply sort lhs rhs + case sequence simplified of + Left _ -> + -- Equation engine error: route to Unsure + -- rather than the old hard 'Aborted', so the + -- client can escalate via kore fallback. + unsure + Right reduced + | all (== Predicate TrueBool) reduced -> + impliesResult + | otherwise -> do + let residue = + Set.fromList $ + filter (/= Predicate TrueBool) reduced + SMT.checkPredicates + solver + antecedentPreds + patL.substitution + residue + >>= \case + SMT.IsValid -> impliesResult + SMT.IsInvalid -> disjoint + -- Vacuous antecedent: any consequent + -- is implied. + SMT.IsUnknown SMT.InconsistentGroundTruth -> + impliesResult + SMT.IsUnknown _ -> unsure case (internalised antecedent.term, internalised consequent.term) of (Left patternError, _) -> do @@ -204,42 +240,46 @@ runImplies def mLlvmLibrary mSMTOptions antecedent consequent = antecedent.term consequent.term where - doesNotImply' s condition l r = - pure $ - Right $ - RpcTypes.Implies - RpcTypes.ImpliesResult - { implication = addHeader $ Kore.Syntax.KJImplies s l r - , valid = False - , condition - , logs = Nothing - , haskellLogEntries = Nothing - } + -- Single construction point for every implies / does-not-imply result. + -- The call sites differ only in 'status' and 'condition'; centralising + -- the record keeps a future field addition a one-line change. + mkResult s l r status condition = + pure . Right . RpcTypes.Implies $ + RpcTypes.ImpliesResult + { implication = addHeader $ Kore.Syntax.KJImplies s l r + , status + , condition + , logs = Nothing + , haskellLogEntries = Nothing + } + + doesNotImply' s condition l r = mkResult s l r RpcTypes.Invalid condition doesNotImply s' = let s = externaliseSort s' in doesNotImply' s Nothing + + -- Variant of 'doesNotImply' that flags the result as indeterminate. + -- Use at non-decisive not-implied outcomes — the 'MatchIndeterminate' + -- retry-ladder no-progress fall-through and the 'MatchSuccess' + -- SMT-discharge 'IsUnknown _' branch — so a recover-mode client + -- escalates to kore rather than trusting @status: invalid@. + doesNotImplyIndeterminate s' l r = + let s = externaliseSort s' in mkResult s l r RpcTypes.Indeterminate Nothing + implies' predicate s l r subst = - pure $ - Right $ - RpcTypes.Implies - RpcTypes.ImpliesResult - { implication = addHeader $ Kore.Syntax.KJImplies s l r - , valid = True - , condition = - Just - RpcTypes.Condition - { predicate = addHeader predicate - , substitution = - addHeader - $ ( \case - [] -> Kore.Syntax.KJTop s - [x] -> x - xs -> Kore.Syntax.KJAnd s xs - ) - . map (uncurry $ externaliseSubstitution s) - . Map.toList - $ subst - } - , logs = Nothing - , haskellLogEntries = Nothing - } + mkResult s l r RpcTypes.Valid (Just condition) + where + condition = + RpcTypes.Condition + { predicate = addHeader predicate + , substitution = + addHeader + $ ( \case + [] -> Kore.Syntax.KJTop s + [x] -> x + xs -> Kore.Syntax.KJAnd s xs + ) + . map (uncurry $ externaliseSubstitution s) + . Map.toList + $ subst + } implies s' = let s = externaliseSort s' in implies' (Kore.Syntax.KJTop s) s diff --git a/booster/test/rpc-integration/resources/implies-smt.k b/booster/test/rpc-integration/resources/implies-smt.k new file mode 100644 index 0000000000..a3e8101384 --- /dev/null +++ b/booster/test/rpc-integration/resources/implies-smt.k @@ -0,0 +1,22 @@ +// Minimal definition for exercising booster's `implies` check against +// integer / boolean obligations that need SMT discharge. +// +// The test claims send raw KORE `implies` requests whose antecedent and +// consequent share identical configurations (so the matcher returns +// MatchSuccess) but differ in their attached path-condition predicates. +// The interesting cases are the ones where the leftover consequent +// predicate is *implied* by the antecedent under linear-integer reasoning +// (e.g. `X ` cell containing an `Int` — enough +// to give us a kompiled definition with `_ $PGM:Int + +endmodule diff --git a/booster/test/rpc-integration/resources/implies-smt.kompile b/booster/test/rpc-integration/resources/implies-smt.kompile new file mode 100755 index 0000000000..5ec0c47471 --- /dev/null +++ b/booster/test/rpc-integration/resources/implies-smt.kompile @@ -0,0 +1,6 @@ +#!/usr/bin/env bash +set -euo pipefail +name=$(basename "$0" .kompile) +kompile --backend haskell "$name.k" --syntax-module IMPLIES-SMT +cp "$name-kompiled/definition.kore" "./$name.kore" +rm -r "$name-kompiled" diff --git a/booster/test/rpc-integration/test-3934-smt/response-003.booster-dev b/booster/test/rpc-integration/test-3934-smt/response-003.booster-dev index c0a21b1928..63e072b931 100644 --- a/booster/test/rpc-integration/test-3934-smt/response-003.booster-dev +++ b/booster/test/rpc-integration/test-3934-smt/response-003.booster-dev @@ -2,7 +2,7 @@ "jsonrpc": "2.0", "id": 3, "result": { - "valid": false, + "status": "invalid", "implication": { "format": "KORE", "version": 1, diff --git a/booster/test/rpc-integration/test-3934-smt/response-003.json b/booster/test/rpc-integration/test-3934-smt/response-003.json index e1abe26d60..62e4dfea80 100644 --- a/booster/test/rpc-integration/test-3934-smt/response-003.json +++ b/booster/test/rpc-integration/test-3934-smt/response-003.json @@ -1 +1 @@ -{"jsonrpc":"2.0","id":3,"result":{"valid":false,"implication":{"format":"KORE","version":1,"term":{"tag":"Implies","sort":{"tag":"SortApp","name":"SortGeneratedTopCell","args":[]},"first":{"tag":"And","sort":{"tag":"SortApp","name":"SortGeneratedTopCell","args":[]},"patterns":[{"tag":"App","name":"Lbl'-LT-'generatedTop'-GT-'","sorts":[],"args":[{"tag":"App","name":"Lbl'-LT-'kevm'-GT-'","sorts":[],"args":[{"tag":"App","name":"Lbl'-LT-'k'-GT-'","sorts":[],"args":[{"tag":"App","name":"kseq","sorts":[],"args":[{"tag":"App","name":"inj","sorts":[{"tag":"SortApp","name":"SortInternalOp","args":[]},{"tag":"SortApp","name":"SortKItem","args":[]}],"args":[{"tag":"App","name":"Lbl'UndsUndsUndsUnds'EVM'Unds'InternalOp'Unds'BinStackOp'Unds'Int'Unds'Int","sorts":[],"args":[{"tag":"App","name":"LblJUMPI'Unds'EVM'Unds'BinStackOp","sorts":[],"args":[]},{"tag":"DV","sort":{"tag":"SortApp","name":"SortInt","args":[]},"value":"1569"},{"tag":"App","name":"Lblbool2Word","sorts":[],"args":[{"tag":"App","name":"Lbl'UndsEqlsEqls'Int'Unds'","sorts":[],"args":[{"tag":"EVar","name":"VarN","sort":{"tag":"SortApp","name":"SortInt","args":[]}},{"tag":"DV","sort":{"tag":"SortApp","name":"SortInt","args":[]},"value":"0"}]}]}]}]},{"tag":"App","name":"kseq","sorts":[],"args":[{"tag":"App","name":"Lblexecute","sorts":[],"args":[]},{"tag":"EVar","name":"VarK'Unds'CELL'Unds'de090c3b","sort":{"tag":"SortApp","name":"SortK","args":[]}}]}]}]},{"tag":"App","name":"Lbl'-LT-'exit-code'-GT-'","sorts":[],"args":[{"tag":"EVar","name":"VarEXITCODE'Unds'CELL","sort":{"tag":"SortApp","name":"SortInt","args":[]}}]},{"tag":"App","name":"Lbl'-LT-'mode'-GT-'","sorts":[],"args":[{"tag":"App","name":"LblNORMAL","sorts":[],"args":[]}]},{"tag":"App","name":"Lbl'-LT-'schedule'-GT-'","sorts":[],"args":[{"tag":"App","name":"LblLONDON'Unds'EVM","sorts":[],"args":[]}]},{"tag":"App","name":"Lbl'-LT-'useGas'-GT-'","sorts":[],"args":[{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"true"}]},{"tag":"App","name":"Lbl'-LT-'ethereum'-GT-'","sorts":[],"args":[{"tag":"App","name":"Lbl'-LT-'evm'-GT-'","sorts":[],"args":[{"tag":"App","name":"Lbl'-LT-'output'-GT-'","sorts":[],"args":[{"tag":"EVar","name":"VarOUTPUT'Unds'CELL","sort":{"tag":"SortApp","name":"SortBytes","args":[]}}]},{"tag":"App","name":"Lbl'-LT-'statusCode'-GT-'","sorts":[],"args":[{"tag":"EVar","name":"VarSTATUSCODE'Unds'CELL","sort":{"tag":"SortApp","name":"SortStatusCode","args":[]}}]},{"tag":"App","name":"Lbl'-LT-'callStack'-GT-'","sorts":[],"args":[{"tag":"EVar","name":"VarCALLSTACK'Unds'CELL","sort":{"tag":"SortApp","name":"SortList","args":[]}}]},{"tag":"App","name":"Lbl'-LT-'interimStates'-GT-'","sorts":[],"args":[{"tag":"EVar","name":"VarINTERIMSTATES'Unds'CELL","sort":{"tag":"SortApp","name":"SortList","args":[]}}]},{"tag":"App","name":"Lbl'-LT-'touchedAccounts'-GT-'","sorts":[],"args":[{"tag":"EVar","name":"VarTOUCHEDACCOUNTS'Unds'CELL","sort":{"tag":"SortApp","name":"SortSet","args":[]}}]},{"tag":"App","name":"Lbl'-LT-'callState'-GT-'","sorts":[],"args":[{"tag":"App","name":"Lbl'-LT-'program'-GT-'","sorts":[],"args":[{"tag":"DV","sort":{"tag":"SortApp","name":"SortBytes","args":[]},"value":"`€`@R4€\u0015a\u0000\u0010W`\u0000€ý[P`\u00046\u0010a\u0001,W`\u00005`à\u001c€c]â/\u0007\u0011a\u0000­W€c¡\u0018á\u0002\u0011a\u0000qW€c¡\u0018á\u0002\u0014a\u0002bW€cºAO¦\u0014a\u0002uW€cÓ\u0013”\r\u0014a\u0002W€cøÌ¿G\u0014a\u0002 W€cúv&Ô\u0014a\u0002³W`\u0000€ý[€c]â/\u0007\u0014a\u0002\u0003W€cm]9ß\u0014a\u0002\u0016W€c~Ž#Ð\u0014a\u0002)W€cˆ~OÛ\u0014a\u0002=`\u0000ý[PPPP`\u0000`\u0002‚`\u0001a\u0004‘a\u0013eV[a\u0004™„a\u0013}V[a\u0004£‘a\u00138V[P`\u0000a\u0004°ƒa\u000c`V[Pa\u0003\u0014‚‚a\u000c’V[`\u0000a\u0004ǂa\rqV[P`\u0001`\u0000[ƒQ\u0010€\u0015a\u0004ÛWP[\u0015a\u0005\u0012WƒQ\u0010a\u0004òWa\u0004òa\u0013œV[` \u0002` \u0001\u0001Qƒ\u0010\u0015‘P€€a\u0005\na\u0013LV[‘PPa\u0004ÎV[Pa\u0003\u0014a\t›V[`\u0000a\u0003&`da\u0005‰V[`\u0000a\u00053‚a\rÐV[P`\u0001`\u0000[ƒQ\u0010€\u0015a\u0005GWP[\u0015a\u0005\u0012WƒQ\u0010a\u0005^Wa\u0005^a\u0013œV[` \u0002` \u0001\u0001Qƒ\u0010\u0015‘P€€a\u0005va\u0013LV[‘PPa\u0005:V[`\u0000a\u0002˃a\u000e.V[`@Qc&1ò±`á\u001bRf¸\u0017\u0002à\\\u000bo‚\u0011\u0015`\u0004‚\u0001R`\u0000sq\tpžÏ©\u001a€boó˜hö[\u001dÑ-cLcåb`$\u0001`\u0000`@Q€ƒ\u0003`\u0000‡€;\u0015€\u0015a\u0005âW`\u0000€ý[PZñ\u0015€\u0015a\u0005öW=`\u0000€>=`\u0000ý[PPPP`\u0000[‚\u0015a\u0006!Wa\u0006\rƒ‚a\u0013eV[Pa\u0006\u001a`\u0001„a\u0013!V[’Pa\u0005ýV[’‘PPV[`@Qc&1ò±`á\u001bR`d‚\u0011\u0015`\u0004‚\u0001Rsq\tpžÏ©\u001a€boó˜hö[\u001dÑ-cLcåb`$\u0001`\u0000`@Q€ƒ\u0003`\u0000‡€;\u0015€\u0015a\u0006wW`\u0000€ý[PZñ\u0015€\u0015a\u0006‹W=`\u0000€>=`\u0000ý[PPPP`\u0000`\u0002‚`\u0001a\u0006 ‘a\u0013eV[a\u0006ª„a\u0013}V[a\u0006´‘a\u00138V[P`\u0000a\u0004°ƒa\u000eeV[`\u0000a\u0006̂a\u000eV[P`\u0001€[‚Q\u0010€\u0015a\u0006ßWP[\u0015a\u0005\u0012WƒQ\u0010a\u0006öWa\u0006öa\u0013œV[` \u0002` \u0001\u0001Q„`\u0001ƒa\u0007\u000c‘a\u0013!V[Q\u0010a\u0007\u001cWa\u0007\u001ca\u0013œV[` \u0002` \u0001\u0001Q\u0011\u0015‘P€€a\u00073a\u0013LV[‘PPa\u0006ÒV[`\u0000a\u0007Fƒa\u000e»V[P‚`\u0000\u0003a\u0007[Wa\u0003\u0014`\u0000a\u000c’V[a\u0007ga\u0002݂a\tJV[`\u0000a\u0007|a\u0007w`\u0001†a\u0013!V[a\u000e»V[Pa\u0003ƒ„\u0011\u0015€a\u0007WP‚„\u0010\u0015[€a\u0002ÝWPa\u0007Ÿ„a\tJV[\u0015a\t›V[`\u0000€Ta\u0001\u0000\u0004`ÿ\u0016\u0015a\u0007ÅWP`\u0000Ta\u0001\u0000\u0004`ÿ\u0016V[`\u0000sq\tpžÏ©\u001a€boó˜hö[\u001dÑ-;\u0015a\u0008ËW`@€Qsq\tpžÏ©\u001a€boó˜hö[\u001dÑ-` ‚\u0001Re\u0019˜Z[\u0019Y`Ò\u001b‚„\u0001R‚Q€ƒ\u0003„\u0001R``ƒ\u0001“R`\u0000’‘a\u0008S‘fpÊA\u001dpêÕ\r\\\"\u0007\r¯Ãj×_=Ï^r7²*ޚìđ`€\u0001a\u0013ÞV[`@€Q`\u001f\u0019„\u0003\u0001R‚Ra\u0008m‘a\u0014\u000fV[`\u0000`@Q€ƒ\u0003`\u0000†Zñ‘PP=€`\u0000\u0014a\u0008ªW`@Q‘P`\u001f\u0019`?=\u0001\u0016‚\u0001`@R=‚R=`\u0000` „\u0001>a\u0008¯V[``‘P[P‘PP€€` \u0001Q\u0001a\u0008Ǒa\u0014+V[‘PP[‘PV[`\u0000a\u0008ۂa\u000eõV[P`\u0001€[‚Q\u0010€\u0015a\u0008îWP[\u0015a\u0005\u0012WƒQ\u0010a\t\u0005Wa\t\u0005a\u0013œV[` \u0002` \u0001\u0001Q„`\u0001ƒa\t\u001b‘a\u0013!V[Q\u0010a\t+Wa\t+a\u0013œV[` \u0002` \u0001\u0001Q\u0011\u0015‘P€€a\tBa\u0013LV[‘PPa\u0008áV[`\u0000`\u0002‚\u0010\u0015a\t]WP`\u0000‘PV[`\u0002[‚\u0010\u0015a\t’Wa\tr„a\u0012÷V[\u0015a\t€WP`\u0000’‘PPV[€a\tŠa\u0013LV[‘PPa\t`V[P`\u0001’‘PPV[€a\u0003£WA0O¬Ù2=u±\u001bÍÖ\tË8ïÿý°W\u0010÷Êðé±lmpŸP`@Qa\tÿ` €‚R`\u0017‚\u0001RError: Assertion Failed\u0000\u0000\u0000\u0000\u0000\u0000\u0000\u0000\u0000`@‚\u0001R``\u0001V[`@Q€‘\u0003¡a\u0003£a\u000f\u0017V[`\u0000`\u0000\u0003a\n!WP`\u0000‘PV[[€‘P`\u0002a\n3…„a\u0010#V[a\n=‘a\u0013eV[a\nG‘a\u00138V[P\u0003a\n#W[P‘PV[`\u0000g\rඳ§d\u0000\u0000a\nm`\u0002‚a\u00138V[a\nw„†a\u0013}V[a\n‘a\u0013eV[a\n‹‘a\u00138V[“’PPPV[`\u0000`\u0002‚\u0010\u0015a\n¥WP`\u0000‘PV[`\u0002[a\n³`\u0002„a\u00138V[\u0011a\t’Wa\nÁ„a\u0012÷V[\u0015a\nÑWP`\u0000’‘PPV[€a\nہa\u0013LV[‘PPa\n¨V[€\u0015\u0015‚\u0015\u0015\u0014a\u0004\u0006WA0O¬Ù2=u±\u001bÍÖ\tË8ïÿý°W\u0010÷Êðé±lmpŸP`@Qa\u000bX` €‚R`\"‚\u0001RError: a == b not satisfied [boo`@‚\u0001Ral]`ð\u001b``‚\u0001R`€\u0001V[`@Q€‘\u0003¡(\u000fDF²Š\u0013rA}Úe0¹[)’±*ÉÇóxS_)©zÏ5ƒa\u000b©W`@Q€`@\u0001`@R€`\u0005R` \u0001dfalse`Ø\u001bRPa\u000bÇV[`@Q€`@\u0001`@R€`\u0004R` \u0001ctrue`à\u001bRP[`@Qa\u000bԑa\u0014yV[`@Q€‘\u0003¡(\u000fDF²Š\u0013rA}Úe0¹[)’±*ÉÇóxS_)©zÏ5ƒ‚a\u000c%W`@Q€`@\u0001`@R€`\u0005R` \u0001dfalse`Ø\u001bRPa\u000cCV[`@Q€`@\u0001`@R€`\u0004R` \u0001ctrue`à\u001bRP[`@Qa\u000cP‘a\u0014½V[`@Q€‘\u0003¡a\u0004\u0006a\u000f\u0017V[`\u0000€€[ƒ\u0010\u0015a\u000c‹Wa\u000cwƒa\u0013eV[‘P€a\u000cƒa\u0013LV[‘PPa\u000ceV[P’‘PPV[€‚\u0014a\u0004\u0006WA0O¬Ù2=u±\u001bÍÖ\tË8ïÿý°W\u0010÷Êðé±lmpŸP`@Qa\r\u0003` €‚R`\"‚\u0001RError: a == b not satisfied [uin`@‚\u0001Rat]`ð\u001b``‚\u0001R`€\u0001V[`@Q€‘\u0003¡²Þ/¾€\u001a\röÀËÝýD‹£Ä\u001dH @Ê5Ål–ï\u000fÊç!¨`@Qa\r:‘a\u0014çV[`@Q€‘\u0003¡²Þ/¾€\u001a\röÀËÝýD‹£Ä\u001dH @Ê5Ål–ï\u000fÊç!¨‚`@Qa\u000cP‘a\u0015\u001fV[`\u0000€`\u0001[ƒQ\u0010\u0015a\u000c‹W„‚Q\u0010a\r“Wa\r“a\u0013œV[` \u0002` \u0001\u0001Q\u0011\u0015a\r¾WƒQ\u0010a\r³Wa\r³a\u0013œV[` \u0002` \u0001\u0001Q‘P[€a\rȁa\u0013LV[‘PPa\rwV[`\u0000€€[ƒQ\u0010\u0015a\u000c‹W„‚Q\u0010a\rñWa\rña\u0013œV[` \u0002` \u0001\u0001Q\u0011\u0015a\u000e\u001cWƒQ\u0010a\u000e\u0011Wa\u000e\u0011a\u0013œV[` \u0002` \u0001\u0001Q‘P[€a\u000e&a\u0013LV[‘PPa\rÕV[`\u0000`\u0002[‚\u0010\u0015a\t’Wa\u000eE„a\u0012÷V[\u0015a\u000eSWP`\u0000’‘PPV[€a\u000e]a\u0013LV[‘PPa\u000e3V[`\u0000€€[ƒ\u0011a\u000c‹Wa\u000e{ƒa\u0013eV[‘P€a\u000e‡a\u0013LV[‘PPa\u000ejV[```\u0001‚Q\u0011a\u000ežWPV[a\u000e·‚`\u0000`\u0001…Qa\u000e²‘a\u0013!V[a\u0010CV[PV[`\u0000€[‚\u0010\u0015a\nQWa\u000eсa\u0013LV[’PPa\u000e݂a\tJV[\u0015a\u000eðW€a\u000eìa\u0013LV[‘PP[a\u000e¿V[```\u0001‚Q\u0011a\u000f\u0004WPV[a\u000e·‚`\u0001€…Qa\u000e²‘a\u0013!V[sq\tpžÏ©\u001a€boó˜hö[\u001dÑ-;\u0015a\u0010\u0012W`@€Qsq\tpžÏ©\u001a€boó˜hö[\u001dÑ-` ‚\u0001Re\u0019˜Z[\u0019Y`Ò\u001b’‚\u0001’’R`\u0001``‚\u0001R`\u0000‘pÊ\u0010»ÐÛý ©ô±4\u0002Ál± p^\r\u001c\nê±\u000f£S®XoĐ`€\u0001`@€Q`\u001f\u0019„\u0003\u0001R‚Ra\u000f±’‘` \u0001a\u0013ÞV[`@€Q`\u001f\u0019„\u0003\u0001R‚Ra\u000fˑa\u0014\u000fV[`\u0000`@Q€ƒ\u0003`\u0000†Zñ‘PP=€`\u0000\u0014a\u0010\u0008W`@Q‘P`\u001f\u0019`?=\u0001\u0016‚\u0001`@R=‚R=`\u0000` „\u0001>a\u0010\rV[``‘P[PPPP[`\u0000€Taÿ\u0000\u0019\u0016a\u0001\u0000\u0017UV[`\u0000a\u00101`\u0002‚a\u00138V[a\nwg\rඳ§d\u0000\u0000†a\u0013}V[€‚\u0010a\u0010OWPPPV[`\u0000…`\u0002a\u0010`……a\u0013!V[a\u0010j‘a\u00138V[a\u0010t‡a\u0013eV[Q\u0010a\u0010„Wa\u0010„a\u0013œV[` \u0002` \u0001\u0001QP[ƒ\u0011a\u0011¤W[€†„Q\u0010a\u0010ªWa\u0010ªa\u0013œV[` \u0002` \u0001\u0001Q\u0010\u0015a\u0010ÊW‚a\u0010a\u0013LV[“PPa\u0010—V[…‚Q\u0010a\u0010ÜWa\u0010Üa\u0013œV[` \u0002` \u0001\u0001Q\u0010€\u0015a\u0010òWP`\u0000‚\u0011[\u0015a\u0011\tWa\u0011\u0001a\u0015IV[’PPa\u0010ÊV[ƒ\u0011a\u0011ŸW…‚Q\u0010a\u0011\"Wa\u0011\"a\u0013œV[` \u0002` \u0001\u0001Q†„Q\u0010a\u0011=`\u0000ý[PPPP`\u0000`\u0002‚`\u0001a\u0004‘a\u0013eV[a\u0004™„a\u0013}V[a\u0004£‘a\u00138V[P`\u0000a\u0004°ƒa\u000c`V[Pa\u0003\u0014‚‚a\u000c’V[`\u0000a\u0004ǂa\rqV[P`\u0001`\u0000[ƒQ\u0010€\u0015a\u0004ÛWP[\u0015a\u0005\u0012WƒQ\u0010a\u0004òWa\u0004òa\u0013œV[` \u0002` \u0001\u0001Qƒ\u0010\u0015‘P€€a\u0005\na\u0013LV[‘PPa\u0004ÎV[Pa\u0003\u0014a\t›V[`\u0000a\u0003&`da\u0005‰V[`\u0000a\u00053‚a\rÐV[P`\u0001`\u0000[ƒQ\u0010€\u0015a\u0005GWP[\u0015a\u0005\u0012WƒQ\u0010a\u0005^Wa\u0005^a\u0013œV[` \u0002` \u0001\u0001Qƒ\u0010\u0015‘P€€a\u0005va\u0013LV[‘PPa\u0005:V[`\u0000a\u0002˃a\u000e.V[`@Qc&1ò±`á\u001bRf¸\u0017\u0002à\\\u000bo‚\u0011\u0015`\u0004‚\u0001R`\u0000sq\tpžÏ©\u001a€boó˜hö[\u001dÑ-cLcåb`$\u0001`\u0000`@Q€ƒ\u0003`\u0000‡€;\u0015€\u0015a\u0005âW`\u0000€ý[PZñ\u0015€\u0015a\u0005öW=`\u0000€>=`\u0000ý[PPPP`\u0000[‚\u0015a\u0006!Wa\u0006\rƒ‚a\u0013eV[Pa\u0006\u001a`\u0001„a\u0013!V[’Pa\u0005ýV[’‘PPV[`@Qc&1ò±`á\u001bR`d‚\u0011\u0015`\u0004‚\u0001Rsq\tpžÏ©\u001a€boó˜hö[\u001dÑ-cLcåb`$\u0001`\u0000`@Q€ƒ\u0003`\u0000‡€;\u0015€\u0015a\u0006wW`\u0000€ý[PZñ\u0015€\u0015a\u0006‹W=`\u0000€>=`\u0000ý[PPPP`\u0000`\u0002‚`\u0001a\u0006 ‘a\u0013eV[a\u0006ª„a\u0013}V[a\u0006´‘a\u00138V[P`\u0000a\u0004°ƒa\u000eeV[`\u0000a\u0006̂a\u000eV[P`\u0001€[‚Q\u0010€\u0015a\u0006ßWP[\u0015a\u0005\u0012WƒQ\u0010a\u0006öWa\u0006öa\u0013œV[` \u0002` \u0001\u0001Q„`\u0001ƒa\u0007\u000c‘a\u0013!V[Q\u0010a\u0007\u001cWa\u0007\u001ca\u0013œV[` \u0002` \u0001\u0001Q\u0011\u0015‘P€€a\u00073a\u0013LV[‘PPa\u0006ÒV[`\u0000a\u0007Fƒa\u000e»V[P‚`\u0000\u0003a\u0007[Wa\u0003\u0014`\u0000a\u000c’V[a\u0007ga\u0002݂a\tJV[`\u0000a\u0007|a\u0007w`\u0001†a\u0013!V[a\u000e»V[Pa\u0003ƒ„\u0011\u0015€a\u0007WP‚„\u0010\u0015[€a\u0002ÝWPa\u0007Ÿ„a\tJV[\u0015a\t›V[`\u0000€Ta\u0001\u0000\u0004`ÿ\u0016\u0015a\u0007ÅWP`\u0000Ta\u0001\u0000\u0004`ÿ\u0016V[`\u0000sq\tpžÏ©\u001a€boó˜hö[\u001dÑ-;\u0015a\u0008ËW`@€Qsq\tpžÏ©\u001a€boó˜hö[\u001dÑ-` ‚\u0001Re\u0019˜Z[\u0019Y`Ò\u001b‚„\u0001R‚Q€ƒ\u0003„\u0001R``ƒ\u0001“R`\u0000’‘a\u0008S‘fpÊA\u001dpêÕ\r\\\"\u0007\r¯Ãj×_=Ï^r7²*ޚìđ`€\u0001a\u0013ÞV[`@€Q`\u001f\u0019„\u0003\u0001R‚Ra\u0008m‘a\u0014\u000fV[`\u0000`@Q€ƒ\u0003`\u0000†Zñ‘PP=€`\u0000\u0014a\u0008ªW`@Q‘P`\u001f\u0019`?=\u0001\u0016‚\u0001`@R=‚R=`\u0000` „\u0001>a\u0008¯V[``‘P[P‘PP€€` \u0001Q\u0001a\u0008Ǒa\u0014+V[‘PP[‘PV[`\u0000a\u0008ۂa\u000eõV[P`\u0001€[‚Q\u0010€\u0015a\u0008îWP[\u0015a\u0005\u0012WƒQ\u0010a\t\u0005Wa\t\u0005a\u0013œV[` \u0002` \u0001\u0001Q„`\u0001ƒa\t\u001b‘a\u0013!V[Q\u0010a\t+Wa\t+a\u0013œV[` \u0002` \u0001\u0001Q\u0011\u0015‘P€€a\tBa\u0013LV[‘PPa\u0008áV[`\u0000`\u0002‚\u0010\u0015a\t]WP`\u0000‘PV[`\u0002[‚\u0010\u0015a\t’Wa\tr„a\u0012÷V[\u0015a\t€WP`\u0000’‘PPV[€a\tŠa\u0013LV[‘PPa\t`V[P`\u0001’‘PPV[€a\u0003£WA0O¬Ù2=u±\u001bÍÖ\tË8ïÿý°W\u0010÷Êðé±lmpŸP`@Qa\tÿ` €‚R`\u0017‚\u0001RError: Assertion Failed\u0000\u0000\u0000\u0000\u0000\u0000\u0000\u0000\u0000`@‚\u0001R``\u0001V[`@Q€‘\u0003¡a\u0003£a\u000f\u0017V[`\u0000`\u0000\u0003a\n!WP`\u0000‘PV[[€‘P`\u0002a\n3…„a\u0010#V[a\n=‘a\u0013eV[a\nG‘a\u00138V[P\u0003a\n#W[P‘PV[`\u0000g\rඳ§d\u0000\u0000a\nm`\u0002‚a\u00138V[a\nw„†a\u0013}V[a\n‘a\u0013eV[a\n‹‘a\u00138V[“’PPPV[`\u0000`\u0002‚\u0010\u0015a\n¥WP`\u0000‘PV[`\u0002[a\n³`\u0002„a\u00138V[\u0011a\t’Wa\nÁ„a\u0012÷V[\u0015a\nÑWP`\u0000’‘PPV[€a\nہa\u0013LV[‘PPa\n¨V[€\u0015\u0015‚\u0015\u0015\u0014a\u0004\u0006WA0O¬Ù2=u±\u001bÍÖ\tË8ïÿý°W\u0010÷Êðé±lmpŸP`@Qa\u000bX` €‚R`\"‚\u0001RError: a == b not satisfied [boo`@‚\u0001Ral]`ð\u001b``‚\u0001R`€\u0001V[`@Q€‘\u0003¡(\u000fDF²Š\u0013rA}Úe0¹[)’±*ÉÇóxS_)©zÏ5ƒa\u000b©W`@Q€`@\u0001`@R€`\u0005R` \u0001dfalse`Ø\u001bRPa\u000bÇV[`@Q€`@\u0001`@R€`\u0004R` \u0001ctrue`à\u001bRP[`@Qa\u000bԑa\u0014yV[`@Q€‘\u0003¡(\u000fDF²Š\u0013rA}Úe0¹[)’±*ÉÇóxS_)©zÏ5ƒ‚a\u000c%W`@Q€`@\u0001`@R€`\u0005R` \u0001dfalse`Ø\u001bRPa\u000cCV[`@Q€`@\u0001`@R€`\u0004R` \u0001ctrue`à\u001bRP[`@Qa\u000cP‘a\u0014½V[`@Q€‘\u0003¡a\u0004\u0006a\u000f\u0017V[`\u0000€€[ƒ\u0010\u0015a\u000c‹Wa\u000cwƒa\u0013eV[‘P€a\u000cƒa\u0013LV[‘PPa\u000ceV[P’‘PPV[€‚\u0014a\u0004\u0006WA0O¬Ù2=u±\u001bÍÖ\tË8ïÿý°W\u0010÷Êðé±lmpŸP`@Qa\r\u0003` €‚R`\"‚\u0001RError: a == b not satisfied [uin`@‚\u0001Rat]`ð\u001b``‚\u0001R`€\u0001V[`@Q€‘\u0003¡²Þ/¾€\u001a\röÀËÝýD‹£Ä\u001dH @Ê5Ål–ï\u000fÊç!¨`@Qa\r:‘a\u0014çV[`@Q€‘\u0003¡²Þ/¾€\u001a\röÀËÝýD‹£Ä\u001dH @Ê5Ål–ï\u000fÊç!¨‚`@Qa\u000cP‘a\u0015\u001fV[`\u0000€`\u0001[ƒQ\u0010\u0015a\u000c‹W„‚Q\u0010a\r“Wa\r“a\u0013œV[` \u0002` \u0001\u0001Q\u0011\u0015a\r¾WƒQ\u0010a\r³Wa\r³a\u0013œV[` \u0002` \u0001\u0001Q‘P[€a\rȁa\u0013LV[‘PPa\rwV[`\u0000€€[ƒQ\u0010\u0015a\u000c‹W„‚Q\u0010a\rñWa\rña\u0013œV[` \u0002` \u0001\u0001Q\u0011\u0015a\u000e\u001cWƒQ\u0010a\u000e\u0011Wa\u000e\u0011a\u0013œV[` \u0002` \u0001\u0001Q‘P[€a\u000e&a\u0013LV[‘PPa\rÕV[`\u0000`\u0002[‚\u0010\u0015a\t’Wa\u000eE„a\u0012÷V[\u0015a\u000eSWP`\u0000’‘PPV[€a\u000e]a\u0013LV[‘PPa\u000e3V[`\u0000€€[ƒ\u0011a\u000c‹Wa\u000e{ƒa\u0013eV[‘P€a\u000e‡a\u0013LV[‘PPa\u000ejV[```\u0001‚Q\u0011a\u000ežWPV[a\u000e·‚`\u0000`\u0001…Qa\u000e²‘a\u0013!V[a\u0010CV[PV[`\u0000€[‚\u0010\u0015a\nQWa\u000eсa\u0013LV[’PPa\u000e݂a\tJV[\u0015a\u000eðW€a\u000eìa\u0013LV[‘PP[a\u000e¿V[```\u0001‚Q\u0011a\u000f\u0004WPV[a\u000e·‚`\u0001€…Qa\u000e²‘a\u0013!V[sq\tpžÏ©\u001a€boó˜hö[\u001dÑ-;\u0015a\u0010\u0012W`@€Qsq\tpžÏ©\u001a€boó˜hö[\u001dÑ-` ‚\u0001Re\u0019˜Z[\u0019Y`Ò\u001b’‚\u0001’’R`\u0001``‚\u0001R`\u0000‘pÊ\u0010»ÐÛý ©ô±4\u0002Ál± p^\r\u001c\nê±\u000f£S®XoĐ`€\u0001`@€Q`\u001f\u0019„\u0003\u0001R‚Ra\u000f±’‘` \u0001a\u0013ÞV[`@€Q`\u001f\u0019„\u0003\u0001R‚Ra\u000fˑa\u0014\u000fV[`\u0000`@Q€ƒ\u0003`\u0000†Zñ‘PP=€`\u0000\u0014a\u0010\u0008W`@Q‘P`\u001f\u0019`?=\u0001\u0016‚\u0001`@R=‚R=`\u0000` „\u0001>a\u0010\rV[``‘P[PPPP[`\u0000€Taÿ\u0000\u0019\u0016a\u0001\u0000\u0017UV[`\u0000a\u00101`\u0002‚a\u00138V[a\nwg\rඳ§d\u0000\u0000†a\u0013}V[€‚\u0010a\u0010OWPPPV[`\u0000…`\u0002a\u0010`……a\u0013!V[a\u0010j‘a\u00138V[a\u0010t‡a\u0013eV[Q\u0010a\u0010„Wa\u0010„a\u0013œV[` \u0002` \u0001\u0001QP[ƒ\u0011a\u0011¤W[€†„Q\u0010a\u0010ªWa\u0010ªa\u0013œV[` \u0002` \u0001\u0001Q\u0010\u0015a\u0010ÊW‚a\u0010a\u0013LV[“PPa\u0010—V[…‚Q\u0010a\u0010ÜWa\u0010Üa\u0013œV[` \u0002` \u0001\u0001Q\u0010€\u0015a\u0010òWP`\u0000‚\u0011[\u0015a\u0011\tWa\u0011\u0001a\u0015IV[’PPa\u0010ÊV[ƒ\u0011a\u0011ŸW…‚Q\u0010a\u0011\"Wa\u0011\"a\u0013œV[` \u0002` \u0001\u0001Q†„Q\u0010a\u0011=`\u0000ý[PPPP`\u0000`\u0002‚`\u0001a\u0004‘a\u0013eV[a\u0004™„a\u0013}V[a\u0004£‘a\u00138V[P`\u0000a\u0004°ƒa\u000c`V[Pa\u0003\u0014‚‚a\u000c’V[`\u0000a\u0004ǂa\rqV[P`\u0001`\u0000[ƒQ\u0010€\u0015a\u0004ÛWP[\u0015a\u0005\u0012WƒQ\u0010a\u0004òWa\u0004òa\u0013œV[` \u0002` \u0001\u0001Qƒ\u0010\u0015‘P€€a\u0005\na\u0013LV[‘PPa\u0004ÎV[Pa\u0003\u0014a\t›V[`\u0000a\u0003&`da\u0005‰V[`\u0000a\u00053‚a\rÐV[P`\u0001`\u0000[ƒQ\u0010€\u0015a\u0005GWP[\u0015a\u0005\u0012WƒQ\u0010a\u0005^Wa\u0005^a\u0013œV[` \u0002` \u0001\u0001Qƒ\u0010\u0015‘P€€a\u0005va\u0013LV[‘PPa\u0005:V[`\u0000a\u0002˃a\u000e.V[`@Qc&1ò±`á\u001bRf¸\u0017\u0002à\\\u000bo‚\u0011\u0015`\u0004‚\u0001R`\u0000sq\tpžÏ©\u001a€boó˜hö[\u001dÑ-cLcåb`$\u0001`\u0000`@Q€ƒ\u0003`\u0000‡€;\u0015€\u0015a\u0005âW`\u0000€ý[PZñ\u0015€\u0015a\u0005öW=`\u0000€>=`\u0000ý[PPPP`\u0000[‚\u0015a\u0006!Wa\u0006\rƒ‚a\u0013eV[Pa\u0006\u001a`\u0001„a\u0013!V[’Pa\u0005ýV[’‘PPV[`@Qc&1ò±`á\u001bR`d‚\u0011\u0015`\u0004‚\u0001Rsq\tpžÏ©\u001a€boó˜hö[\u001dÑ-cLcåb`$\u0001`\u0000`@Q€ƒ\u0003`\u0000‡€;\u0015€\u0015a\u0006wW`\u0000€ý[PZñ\u0015€\u0015a\u0006‹W=`\u0000€>=`\u0000ý[PPPP`\u0000`\u0002‚`\u0001a\u0006 ‘a\u0013eV[a\u0006ª„a\u0013}V[a\u0006´‘a\u00138V[P`\u0000a\u0004°ƒa\u000eeV[`\u0000a\u0006̂a\u000eV[P`\u0001€[‚Q\u0010€\u0015a\u0006ßWP[\u0015a\u0005\u0012WƒQ\u0010a\u0006öWa\u0006öa\u0013œV[` \u0002` \u0001\u0001Q„`\u0001ƒa\u0007\u000c‘a\u0013!V[Q\u0010a\u0007\u001cWa\u0007\u001ca\u0013œV[` \u0002` \u0001\u0001Q\u0011\u0015‘P€€a\u00073a\u0013LV[‘PPa\u0006ÒV[`\u0000a\u0007Fƒa\u000e»V[P‚`\u0000\u0003a\u0007[Wa\u0003\u0014`\u0000a\u000c’V[a\u0007ga\u0002݂a\tJV[`\u0000a\u0007|a\u0007w`\u0001†a\u0013!V[a\u000e»V[Pa\u0003ƒ„\u0011\u0015€a\u0007WP‚„\u0010\u0015[€a\u0002ÝWPa\u0007Ÿ„a\tJV[\u0015a\t›V[`\u0000€Ta\u0001\u0000\u0004`ÿ\u0016\u0015a\u0007ÅWP`\u0000Ta\u0001\u0000\u0004`ÿ\u0016V[`\u0000sq\tpžÏ©\u001a€boó˜hö[\u001dÑ-;\u0015a\u0008ËW`@€Qsq\tpžÏ©\u001a€boó˜hö[\u001dÑ-` ‚\u0001Re\u0019˜Z[\u0019Y`Ò\u001b‚„\u0001R‚Q€ƒ\u0003„\u0001R``ƒ\u0001“R`\u0000’‘a\u0008S‘fpÊA\u001dpêÕ\r\\\"\u0007\r¯Ãj×_=Ï^r7²*ޚìđ`€\u0001a\u0013ÞV[`@€Q`\u001f\u0019„\u0003\u0001R‚Ra\u0008m‘a\u0014\u000fV[`\u0000`@Q€ƒ\u0003`\u0000†Zñ‘PP=€`\u0000\u0014a\u0008ªW`@Q‘P`\u001f\u0019`?=\u0001\u0016‚\u0001`@R=‚R=`\u0000` „\u0001>a\u0008¯V[``‘P[P‘PP€€` \u0001Q\u0001a\u0008Ǒa\u0014+V[‘PP[‘PV[`\u0000a\u0008ۂa\u000eõV[P`\u0001€[‚Q\u0010€\u0015a\u0008îWP[\u0015a\u0005\u0012WƒQ\u0010a\t\u0005Wa\t\u0005a\u0013œV[` \u0002` \u0001\u0001Q„`\u0001ƒa\t\u001b‘a\u0013!V[Q\u0010a\t+Wa\t+a\u0013œV[` \u0002` \u0001\u0001Q\u0011\u0015‘P€€a\tBa\u0013LV[‘PPa\u0008áV[`\u0000`\u0002‚\u0010\u0015a\t]WP`\u0000‘PV[`\u0002[‚\u0010\u0015a\t’Wa\tr„a\u0012÷V[\u0015a\t€WP`\u0000’‘PPV[€a\tŠa\u0013LV[‘PPa\t`V[P`\u0001’‘PPV[€a\u0003£WA0O¬Ù2=u±\u001bÍÖ\tË8ïÿý°W\u0010÷Êðé±lmpŸP`@Qa\tÿ` €‚R`\u0017‚\u0001RError: Assertion Failed\u0000\u0000\u0000\u0000\u0000\u0000\u0000\u0000\u0000`@‚\u0001R``\u0001V[`@Q€‘\u0003¡a\u0003£a\u000f\u0017V[`\u0000`\u0000\u0003a\n!WP`\u0000‘PV[[€‘P`\u0002a\n3…„a\u0010#V[a\n=‘a\u0013eV[a\nG‘a\u00138V[P\u0003a\n#W[P‘PV[`\u0000g\rඳ§d\u0000\u0000a\nm`\u0002‚a\u00138V[a\nw„†a\u0013}V[a\n‘a\u0013eV[a\n‹‘a\u00138V[“’PPPV[`\u0000`\u0002‚\u0010\u0015a\n¥WP`\u0000‘PV[`\u0002[a\n³`\u0002„a\u00138V[\u0011a\t’Wa\nÁ„a\u0012÷V[\u0015a\nÑWP`\u0000’‘PPV[€a\nہa\u0013LV[‘PPa\n¨V[€\u0015\u0015‚\u0015\u0015\u0014a\u0004\u0006WA0O¬Ù2=u±\u001bÍÖ\tË8ïÿý°W\u0010÷Êðé±lmpŸP`@Qa\u000bX` €‚R`\"‚\u0001RError: a == b not satisfied [boo`@‚\u0001Ral]`ð\u001b``‚\u0001R`€\u0001V[`@Q€‘\u0003¡(\u000fDF²Š\u0013rA}Úe0¹[)’±*ÉÇóxS_)©zÏ5ƒa\u000b©W`@Q€`@\u0001`@R€`\u0005R` \u0001dfalse`Ø\u001bRPa\u000bÇV[`@Q€`@\u0001`@R€`\u0004R` \u0001ctrue`à\u001bRP[`@Qa\u000bԑa\u0014yV[`@Q€‘\u0003¡(\u000fDF²Š\u0013rA}Úe0¹[)’±*ÉÇóxS_)©zÏ5ƒ‚a\u000c%W`@Q€`@\u0001`@R€`\u0005R` \u0001dfalse`Ø\u001bRPa\u000cCV[`@Q€`@\u0001`@R€`\u0004R` \u0001ctrue`à\u001bRP[`@Qa\u000cP‘a\u0014½V[`@Q€‘\u0003¡a\u0004\u0006a\u000f\u0017V[`\u0000€€[ƒ\u0010\u0015a\u000c‹Wa\u000cwƒa\u0013eV[‘P€a\u000cƒa\u0013LV[‘PPa\u000ceV[P’‘PPV[€‚\u0014a\u0004\u0006WA0O¬Ù2=u±\u001bÍÖ\tË8ïÿý°W\u0010÷Êðé±lmpŸP`@Qa\r\u0003` €‚R`\"‚\u0001RError: a == b not satisfied [uin`@‚\u0001Rat]`ð\u001b``‚\u0001R`€\u0001V[`@Q€‘\u0003¡²Þ/¾€\u001a\röÀËÝýD‹£Ä\u001dH @Ê5Ål–ï\u000fÊç!¨`@Qa\r:‘a\u0014çV[`@Q€‘\u0003¡²Þ/¾€\u001a\röÀËÝýD‹£Ä\u001dH @Ê5Ål–ï\u000fÊç!¨‚`@Qa\u000cP‘a\u0015\u001fV[`\u0000€`\u0001[ƒQ\u0010\u0015a\u000c‹W„‚Q\u0010a\r“Wa\r“a\u0013œV[` \u0002` \u0001\u0001Q\u0011\u0015a\r¾WƒQ\u0010a\r³Wa\r³a\u0013œV[` \u0002` \u0001\u0001Q‘P[€a\rȁa\u0013LV[‘PPa\rwV[`\u0000€€[ƒQ\u0010\u0015a\u000c‹W„‚Q\u0010a\rñWa\rña\u0013œV[` \u0002` \u0001\u0001Q\u0011\u0015a\u000e\u001cWƒQ\u0010a\u000e\u0011Wa\u000e\u0011a\u0013œV[` \u0002` \u0001\u0001Q‘P[€a\u000e&a\u0013LV[‘PPa\rÕV[`\u0000`\u0002[‚\u0010\u0015a\t’Wa\u000eE„a\u0012÷V[\u0015a\u000eSWP`\u0000’‘PPV[€a\u000e]a\u0013LV[‘PPa\u000e3V[`\u0000€€[ƒ\u0011a\u000c‹Wa\u000e{ƒa\u0013eV[‘P€a\u000e‡a\u0013LV[‘PPa\u000ejV[```\u0001‚Q\u0011a\u000ežWPV[a\u000e·‚`\u0000`\u0001…Qa\u000e²‘a\u0013!V[a\u0010CV[PV[`\u0000€[‚\u0010\u0015a\nQWa\u000eсa\u0013LV[’PPa\u000e݂a\tJV[\u0015a\u000eðW€a\u000eìa\u0013LV[‘PP[a\u000e¿V[```\u0001‚Q\u0011a\u000f\u0004WPV[a\u000e·‚`\u0001€…Qa\u000e²‘a\u0013!V[sq\tpžÏ©\u001a€boó˜hö[\u001dÑ-;\u0015a\u0010\u0012W`@€Qsq\tpžÏ©\u001a€boó˜hö[\u001dÑ-` ‚\u0001Re\u0019˜Z[\u0019Y`Ò\u001b’‚\u0001’’R`\u0001``‚\u0001R`\u0000‘pÊ\u0010»ÐÛý ©ô±4\u0002Ál± p^\r\u001c\nê±\u000f£S®XoĐ`€\u0001`@€Q`\u001f\u0019„\u0003\u0001R‚Ra\u000f±’‘` \u0001a\u0013ÞV[`@€Q`\u001f\u0019„\u0003\u0001R‚Ra\u000fˑa\u0014\u000fV[`\u0000`@Q€ƒ\u0003`\u0000†Zñ‘PP=€`\u0000\u0014a\u0010\u0008W`@Q‘P`\u001f\u0019`?=\u0001\u0016‚\u0001`@R=‚R=`\u0000` „\u0001>a\u0010\rV[``‘P[PPPP[`\u0000€Taÿ\u0000\u0019\u0016a\u0001\u0000\u0017UV[`\u0000a\u00101`\u0002‚a\u00138V[a\nwg\rඳ§d\u0000\u0000†a\u0013}V[€‚\u0010a\u0010OWPPPV[`\u0000…`\u0002a\u0010`……a\u0013!V[a\u0010j‘a\u00138V[a\u0010t‡a\u0013eV[Q\u0010a\u0010„Wa\u0010„a\u0013œV[` \u0002` \u0001\u0001QP[ƒ\u0011a\u0011¤W[€†„Q\u0010a\u0010ªWa\u0010ªa\u0013œV[` \u0002` \u0001\u0001Q\u0010\u0015a\u0010ÊW‚a\u0010a\u0013LV[“PPa\u0010—V[…‚Q\u0010a\u0010ÜWa\u0010Üa\u0013œV[` \u0002` \u0001\u0001Q\u0010€\u0015a\u0010òWP`\u0000‚\u0011[\u0015a\u0011\tWa\u0011\u0001a\u0015IV[’PPa\u0010ÊV[ƒ\u0011a\u0011ŸW…‚Q\u0010a\u0011\"Wa\u0011\"a\u0013œV[` \u0002` \u0001\u0001Q†„Q\u0010a\u0011=`\u0000ý[PPPP`\u0000`\u0002‚`\u0001a\u0004‘a\u0013eV[a\u0004™„a\u0013}V[a\u0004£‘a\u00138V[P`\u0000a\u0004°ƒa\u000c`V[Pa\u0003\u0014‚‚a\u000c’V[`\u0000a\u0004ǂa\rqV[P`\u0001`\u0000[ƒQ\u0010€\u0015a\u0004ÛWP[\u0015a\u0005\u0012WƒQ\u0010a\u0004òWa\u0004òa\u0013œV[` \u0002` \u0001\u0001Qƒ\u0010\u0015‘P€€a\u0005\na\u0013LV[‘PPa\u0004ÎV[Pa\u0003\u0014a\t›V[`\u0000a\u0003&`da\u0005‰V[`\u0000a\u00053‚a\rÐV[P`\u0001`\u0000[ƒQ\u0010€\u0015a\u0005GWP[\u0015a\u0005\u0012WƒQ\u0010a\u0005^Wa\u0005^a\u0013œV[` \u0002` \u0001\u0001Qƒ\u0010\u0015‘P€€a\u0005va\u0013LV[‘PPa\u0005:V[`\u0000a\u0002˃a\u000e.V[`@Qc&1ò±`á\u001bRf¸\u0017\u0002à\\\u000bo‚\u0011\u0015`\u0004‚\u0001R`\u0000sq\tpžÏ©\u001a€boó˜hö[\u001dÑ-cLcåb`$\u0001`\u0000`@Q€ƒ\u0003`\u0000‡€;\u0015€\u0015a\u0005âW`\u0000€ý[PZñ\u0015€\u0015a\u0005öW=`\u0000€>=`\u0000ý[PPPP`\u0000[‚\u0015a\u0006!Wa\u0006\rƒ‚a\u0013eV[Pa\u0006\u001a`\u0001„a\u0013!V[’Pa\u0005ýV[’‘PPV[`@Qc&1ò±`á\u001bR`d‚\u0011\u0015`\u0004‚\u0001Rsq\tpžÏ©\u001a€boó˜hö[\u001dÑ-cLcåb`$\u0001`\u0000`@Q€ƒ\u0003`\u0000‡€;\u0015€\u0015a\u0006wW`\u0000€ý[PZñ\u0015€\u0015a\u0006‹W=`\u0000€>=`\u0000ý[PPPP`\u0000`\u0002‚`\u0001a\u0006 ‘a\u0013eV[a\u0006ª„a\u0013}V[a\u0006´‘a\u00138V[P`\u0000a\u0004°ƒa\u000eeV[`\u0000a\u0006̂a\u000eV[P`\u0001€[‚Q\u0010€\u0015a\u0006ßWP[\u0015a\u0005\u0012WƒQ\u0010a\u0006öWa\u0006öa\u0013œV[` \u0002` \u0001\u0001Q„`\u0001ƒa\u0007\u000c‘a\u0013!V[Q\u0010a\u0007\u001cWa\u0007\u001ca\u0013œV[` \u0002` \u0001\u0001Q\u0011\u0015‘P€€a\u00073a\u0013LV[‘PPa\u0006ÒV[`\u0000a\u0007Fƒa\u000e»V[P‚`\u0000\u0003a\u0007[Wa\u0003\u0014`\u0000a\u000c’V[a\u0007ga\u0002݂a\tJV[`\u0000a\u0007|a\u0007w`\u0001†a\u0013!V[a\u000e»V[Pa\u0003ƒ„\u0011\u0015€a\u0007WP‚„\u0010\u0015[€a\u0002ÝWPa\u0007Ÿ„a\tJV[\u0015a\t›V[`\u0000€Ta\u0001\u0000\u0004`ÿ\u0016\u0015a\u0007ÅWP`\u0000Ta\u0001\u0000\u0004`ÿ\u0016V[`\u0000sq\tpžÏ©\u001a€boó˜hö[\u001dÑ-;\u0015a\u0008ËW`@€Qsq\tpžÏ©\u001a€boó˜hö[\u001dÑ-` ‚\u0001Re\u0019˜Z[\u0019Y`Ò\u001b‚„\u0001R‚Q€ƒ\u0003„\u0001R``ƒ\u0001“R`\u0000’‘a\u0008S‘fpÊA\u001dpêÕ\r\\\"\u0007\r¯Ãj×_=Ï^r7²*ޚìđ`€\u0001a\u0013ÞV[`@€Q`\u001f\u0019„\u0003\u0001R‚Ra\u0008m‘a\u0014\u000fV[`\u0000`@Q€ƒ\u0003`\u0000†Zñ‘PP=€`\u0000\u0014a\u0008ªW`@Q‘P`\u001f\u0019`?=\u0001\u0016‚\u0001`@R=‚R=`\u0000` „\u0001>a\u0008¯V[``‘P[P‘PP€€` \u0001Q\u0001a\u0008Ǒa\u0014+V[‘PP[‘PV[`\u0000a\u0008ۂa\u000eõV[P`\u0001€[‚Q\u0010€\u0015a\u0008îWP[\u0015a\u0005\u0012WƒQ\u0010a\t\u0005Wa\t\u0005a\u0013œV[` \u0002` \u0001\u0001Q„`\u0001ƒa\t\u001b‘a\u0013!V[Q\u0010a\t+Wa\t+a\u0013œV[` \u0002` \u0001\u0001Q\u0011\u0015‘P€€a\tBa\u0013LV[‘PPa\u0008áV[`\u0000`\u0002‚\u0010\u0015a\t]WP`\u0000‘PV[`\u0002[‚\u0010\u0015a\t’Wa\tr„a\u0012÷V[\u0015a\t€WP`\u0000’‘PPV[€a\tŠa\u0013LV[‘PPa\t`V[P`\u0001’‘PPV[€a\u0003£WA0O¬Ù2=u±\u001bÍÖ\tË8ïÿý°W\u0010÷Êðé±lmpŸP`@Qa\tÿ` €‚R`\u0017‚\u0001RError: Assertion Failed\u0000\u0000\u0000\u0000\u0000\u0000\u0000\u0000\u0000`@‚\u0001R``\u0001V[`@Q€‘\u0003¡a\u0003£a\u000f\u0017V[`\u0000`\u0000\u0003a\n!WP`\u0000‘PV[[€‘P`\u0002a\n3…„a\u0010#V[a\n=‘a\u0013eV[a\nG‘a\u00138V[P\u0003a\n#W[P‘PV[`\u0000g\rඳ§d\u0000\u0000a\nm`\u0002‚a\u00138V[a\nw„†a\u0013}V[a\n‘a\u0013eV[a\n‹‘a\u00138V[“’PPPV[`\u0000`\u0002‚\u0010\u0015a\n¥WP`\u0000‘PV[`\u0002[a\n³`\u0002„a\u00138V[\u0011a\t’Wa\nÁ„a\u0012÷V[\u0015a\nÑWP`\u0000’‘PPV[€a\nہa\u0013LV[‘PPa\n¨V[€\u0015\u0015‚\u0015\u0015\u0014a\u0004\u0006WA0O¬Ù2=u±\u001bÍÖ\tË8ïÿý°W\u0010÷Êðé±lmpŸP`@Qa\u000bX` €‚R`\"‚\u0001RError: a == b not satisfied [boo`@‚\u0001Ral]`ð\u001b``‚\u0001R`€\u0001V[`@Q€‘\u0003¡(\u000fDF²Š\u0013rA}Úe0¹[)’±*ÉÇóxS_)©zÏ5ƒa\u000b©W`@Q€`@\u0001`@R€`\u0005R` \u0001dfalse`Ø\u001bRPa\u000bÇV[`@Q€`@\u0001`@R€`\u0004R` \u0001ctrue`à\u001bRP[`@Qa\u000bԑa\u0014yV[`@Q€‘\u0003¡(\u000fDF²Š\u0013rA}Úe0¹[)’±*ÉÇóxS_)©zÏ5ƒ‚a\u000c%W`@Q€`@\u0001`@R€`\u0005R` \u0001dfalse`Ø\u001bRPa\u000cCV[`@Q€`@\u0001`@R€`\u0004R` \u0001ctrue`à\u001bRP[`@Qa\u000cP‘a\u0014½V[`@Q€‘\u0003¡a\u0004\u0006a\u000f\u0017V[`\u0000€€[ƒ\u0010\u0015a\u000c‹Wa\u000cwƒa\u0013eV[‘P€a\u000cƒa\u0013LV[‘PPa\u000ceV[P’‘PPV[€‚\u0014a\u0004\u0006WA0O¬Ù2=u±\u001bÍÖ\tË8ïÿý°W\u0010÷Êðé±lmpŸP`@Qa\r\u0003` €‚R`\"‚\u0001RError: a == b not satisfied [uin`@‚\u0001Rat]`ð\u001b``‚\u0001R`€\u0001V[`@Q€‘\u0003¡²Þ/¾€\u001a\röÀËÝýD‹£Ä\u001dH @Ê5Ål–ï\u000fÊç!¨`@Qa\r:‘a\u0014çV[`@Q€‘\u0003¡²Þ/¾€\u001a\röÀËÝýD‹£Ä\u001dH @Ê5Ål–ï\u000fÊç!¨‚`@Qa\u000cP‘a\u0015\u001fV[`\u0000€`\u0001[ƒQ\u0010\u0015a\u000c‹W„‚Q\u0010a\r“Wa\r“a\u0013œV[` \u0002` \u0001\u0001Q\u0011\u0015a\r¾WƒQ\u0010a\r³Wa\r³a\u0013œV[` \u0002` \u0001\u0001Q‘P[€a\rȁa\u0013LV[‘PPa\rwV[`\u0000€€[ƒQ\u0010\u0015a\u000c‹W„‚Q\u0010a\rñWa\rña\u0013œV[` \u0002` \u0001\u0001Q\u0011\u0015a\u000e\u001cWƒQ\u0010a\u000e\u0011Wa\u000e\u0011a\u0013œV[` \u0002` \u0001\u0001Q‘P[€a\u000e&a\u0013LV[‘PPa\rÕV[`\u0000`\u0002[‚\u0010\u0015a\t’Wa\u000eE„a\u0012÷V[\u0015a\u000eSWP`\u0000’‘PPV[€a\u000e]a\u0013LV[‘PPa\u000e3V[`\u0000€€[ƒ\u0011a\u000c‹Wa\u000e{ƒa\u0013eV[‘P€a\u000e‡a\u0013LV[‘PPa\u000ejV[```\u0001‚Q\u0011a\u000ežWPV[a\u000e·‚`\u0000`\u0001…Qa\u000e²‘a\u0013!V[a\u0010CV[PV[`\u0000€[‚\u0010\u0015a\nQWa\u000eсa\u0013LV[’PPa\u000e݂a\tJV[\u0015a\u000eðW€a\u000eìa\u0013LV[‘PP[a\u000e¿V[```\u0001‚Q\u0011a\u000f\u0004WPV[a\u000e·‚`\u0001€…Qa\u000e²‘a\u0013!V[sq\tpžÏ©\u001a€boó˜hö[\u001dÑ-;\u0015a\u0010\u0012W`@€Qsq\tpžÏ©\u001a€boó˜hö[\u001dÑ-` ‚\u0001Re\u0019˜Z[\u0019Y`Ò\u001b’‚\u0001’’R`\u0001``‚\u0001R`\u0000‘pÊ\u0010»ÐÛý ©ô±4\u0002Ál± p^\r\u001c\nê±\u000f£S®XoĐ`€\u0001`@€Q`\u001f\u0019„\u0003\u0001R‚Ra\u000f±’‘` \u0001a\u0013ÞV[`@€Q`\u001f\u0019„\u0003\u0001R‚Ra\u000fˑa\u0014\u000fV[`\u0000`@Q€ƒ\u0003`\u0000†Zñ‘PP=€`\u0000\u0014a\u0010\u0008W`@Q‘P`\u001f\u0019`?=\u0001\u0016‚\u0001`@R=‚R=`\u0000` „\u0001>a\u0010\rV[``‘P[PPPP[`\u0000€Taÿ\u0000\u0019\u0016a\u0001\u0000\u0017UV[`\u0000a\u00101`\u0002‚a\u00138V[a\nwg\rඳ§d\u0000\u0000†a\u0013}V[€‚\u0010a\u0010OWPPPV[`\u0000…`\u0002a\u0010`……a\u0013!V[a\u0010j‘a\u00138V[a\u0010t‡a\u0013eV[Q\u0010a\u0010„Wa\u0010„a\u0013œV[` \u0002` \u0001\u0001QP[ƒ\u0011a\u0011¤W[€†„Q\u0010a\u0010ªWa\u0010ªa\u0013œV[` \u0002` \u0001\u0001Q\u0010\u0015a\u0010ÊW‚a\u0010a\u0013LV[“PPa\u0010—V[…‚Q\u0010a\u0010ÜWa\u0010Üa\u0013œV[` \u0002` \u0001\u0001Q\u0010€\u0015a\u0010òWP`\u0000‚\u0011[\u0015a\u0011\tWa\u0011\u0001a\u0015IV[’PPa\u0010ÊV[ƒ\u0011a\u0011ŸW…‚Q\u0010a\u0011\"Wa\u0011\"a\u0013œV[` \u0002` \u0001\u0001Q†„Q\u0010a\u0011=`\u0000ý[PPPP`\u0000`\u0002‚`\u0001a\u0004‘a\u0013eV[a\u0004™„a\u0013}V[a\u0004£‘a\u00138V[P`\u0000a\u0004°ƒa\u000c`V[Pa\u0003\u0014‚‚a\u000c’V[`\u0000a\u0004ǂa\rqV[P`\u0001`\u0000[ƒQ\u0010€\u0015a\u0004ÛWP[\u0015a\u0005\u0012WƒQ\u0010a\u0004òWa\u0004òa\u0013œV[` \u0002` \u0001\u0001Qƒ\u0010\u0015‘P€€a\u0005\na\u0013LV[‘PPa\u0004ÎV[Pa\u0003\u0014a\t›V[`\u0000a\u0003&`da\u0005‰V[`\u0000a\u00053‚a\rÐV[P`\u0001`\u0000[ƒQ\u0010€\u0015a\u0005GWP[\u0015a\u0005\u0012WƒQ\u0010a\u0005^Wa\u0005^a\u0013œV[` \u0002` \u0001\u0001Qƒ\u0010\u0015‘P€€a\u0005va\u0013LV[‘PPa\u0005:V[`\u0000a\u0002˃a\u000e.V[`@Qc&1ò±`á\u001bRf¸\u0017\u0002à\\\u000bo‚\u0011\u0015`\u0004‚\u0001R`\u0000sq\tpžÏ©\u001a€boó˜hö[\u001dÑ-cLcåb`$\u0001`\u0000`@Q€ƒ\u0003`\u0000‡€;\u0015€\u0015a\u0005âW`\u0000€ý[PZñ\u0015€\u0015a\u0005öW=`\u0000€>=`\u0000ý[PPPP`\u0000[‚\u0015a\u0006!Wa\u0006\rƒ‚a\u0013eV[Pa\u0006\u001a`\u0001„a\u0013!V[’Pa\u0005ýV[’‘PPV[`@Qc&1ò±`á\u001bR`d‚\u0011\u0015`\u0004‚\u0001Rsq\tpžÏ©\u001a€boó˜hö[\u001dÑ-cLcåb`$\u0001`\u0000`@Q€ƒ\u0003`\u0000‡€;\u0015€\u0015a\u0006wW`\u0000€ý[PZñ\u0015€\u0015a\u0006‹W=`\u0000€>=`\u0000ý[PPPP`\u0000`\u0002‚`\u0001a\u0006 ‘a\u0013eV[a\u0006ª„a\u0013}V[a\u0006´‘a\u00138V[P`\u0000a\u0004°ƒa\u000eeV[`\u0000a\u0006̂a\u000eV[P`\u0001€[‚Q\u0010€\u0015a\u0006ßWP[\u0015a\u0005\u0012WƒQ\u0010a\u0006öWa\u0006öa\u0013œV[` \u0002` \u0001\u0001Q„`\u0001ƒa\u0007\u000c‘a\u0013!V[Q\u0010a\u0007\u001cWa\u0007\u001ca\u0013œV[` \u0002` \u0001\u0001Q\u0011\u0015‘P€€a\u00073a\u0013LV[‘PPa\u0006ÒV[`\u0000a\u0007Fƒa\u000e»V[P‚`\u0000\u0003a\u0007[Wa\u0003\u0014`\u0000a\u000c’V[a\u0007ga\u0002݂a\tJV[`\u0000a\u0007|a\u0007w`\u0001†a\u0013!V[a\u000e»V[Pa\u0003ƒ„\u0011\u0015€a\u0007WP‚„\u0010\u0015[€a\u0002ÝWPa\u0007Ÿ„a\tJV[\u0015a\t›V[`\u0000€Ta\u0001\u0000\u0004`ÿ\u0016\u0015a\u0007ÅWP`\u0000Ta\u0001\u0000\u0004`ÿ\u0016V[`\u0000sq\tpžÏ©\u001a€boó˜hö[\u001dÑ-;\u0015a\u0008ËW`@€Qsq\tpžÏ©\u001a€boó˜hö[\u001dÑ-` ‚\u0001Re\u0019˜Z[\u0019Y`Ò\u001b‚„\u0001R‚Q€ƒ\u0003„\u0001R``ƒ\u0001“R`\u0000’‘a\u0008S‘fpÊA\u001dpêÕ\r\\\"\u0007\r¯Ãj×_=Ï^r7²*ޚìđ`€\u0001a\u0013ÞV[`@€Q`\u001f\u0019„\u0003\u0001R‚Ra\u0008m‘a\u0014\u000fV[`\u0000`@Q€ƒ\u0003`\u0000†Zñ‘PP=€`\u0000\u0014a\u0008ªW`@Q‘P`\u001f\u0019`?=\u0001\u0016‚\u0001`@R=‚R=`\u0000` „\u0001>a\u0008¯V[``‘P[P‘PP€€` \u0001Q\u0001a\u0008Ǒa\u0014+V[‘PP[‘PV[`\u0000a\u0008ۂa\u000eõV[P`\u0001€[‚Q\u0010€\u0015a\u0008îWP[\u0015a\u0005\u0012WƒQ\u0010a\t\u0005Wa\t\u0005a\u0013œV[` \u0002` \u0001\u0001Q„`\u0001ƒa\t\u001b‘a\u0013!V[Q\u0010a\t+Wa\t+a\u0013œV[` \u0002` \u0001\u0001Q\u0011\u0015‘P€€a\tBa\u0013LV[‘PPa\u0008áV[`\u0000`\u0002‚\u0010\u0015a\t]WP`\u0000‘PV[`\u0002[‚\u0010\u0015a\t’Wa\tr„a\u0012÷V[\u0015a\t€WP`\u0000’‘PPV[€a\tŠa\u0013LV[‘PPa\t`V[P`\u0001’‘PPV[€a\u0003£WA0O¬Ù2=u±\u001bÍÖ\tË8ïÿý°W\u0010÷Êðé±lmpŸP`@Qa\tÿ` €‚R`\u0017‚\u0001RError: Assertion Failed\u0000\u0000\u0000\u0000\u0000\u0000\u0000\u0000\u0000`@‚\u0001R``\u0001V[`@Q€‘\u0003¡a\u0003£a\u000f\u0017V[`\u0000`\u0000\u0003a\n!WP`\u0000‘PV[[€‘P`\u0002a\n3…„a\u0010#V[a\n=‘a\u0013eV[a\nG‘a\u00138V[P\u0003a\n#W[P‘PV[`\u0000g\rඳ§d\u0000\u0000a\nm`\u0002‚a\u00138V[a\nw„†a\u0013}V[a\n‘a\u0013eV[a\n‹‘a\u00138V[“’PPPV[`\u0000`\u0002‚\u0010\u0015a\n¥WP`\u0000‘PV[`\u0002[a\n³`\u0002„a\u00138V[\u0011a\t’Wa\nÁ„a\u0012÷V[\u0015a\nÑWP`\u0000’‘PPV[€a\nہa\u0013LV[‘PPa\n¨V[€\u0015\u0015‚\u0015\u0015\u0014a\u0004\u0006WA0O¬Ù2=u±\u001bÍÖ\tË8ïÿý°W\u0010÷Êðé±lmpŸP`@Qa\u000bX` €‚R`\"‚\u0001RError: a == b not satisfied [boo`@‚\u0001Ral]`ð\u001b``‚\u0001R`€\u0001V[`@Q€‘\u0003¡(\u000fDF²Š\u0013rA}Úe0¹[)’±*ÉÇóxS_)©zÏ5ƒa\u000b©W`@Q€`@\u0001`@R€`\u0005R` \u0001dfalse`Ø\u001bRPa\u000bÇV[`@Q€`@\u0001`@R€`\u0004R` \u0001ctrue`à\u001bRP[`@Qa\u000bԑa\u0014yV[`@Q€‘\u0003¡(\u000fDF²Š\u0013rA}Úe0¹[)’±*ÉÇóxS_)©zÏ5ƒ‚a\u000c%W`@Q€`@\u0001`@R€`\u0005R` \u0001dfalse`Ø\u001bRPa\u000cCV[`@Q€`@\u0001`@R€`\u0004R` \u0001ctrue`à\u001bRP[`@Qa\u000cP‘a\u0014½V[`@Q€‘\u0003¡a\u0004\u0006a\u000f\u0017V[`\u0000€€[ƒ\u0010\u0015a\u000c‹Wa\u000cwƒa\u0013eV[‘P€a\u000cƒa\u0013LV[‘PPa\u000ceV[P’‘PPV[€‚\u0014a\u0004\u0006WA0O¬Ù2=u±\u001bÍÖ\tË8ïÿý°W\u0010÷Êðé±lmpŸP`@Qa\r\u0003` €‚R`\"‚\u0001RError: a == b not satisfied [uin`@‚\u0001Rat]`ð\u001b``‚\u0001R`€\u0001V[`@Q€‘\u0003¡²Þ/¾€\u001a\röÀËÝýD‹£Ä\u001dH @Ê5Ål–ï\u000fÊç!¨`@Qa\r:‘a\u0014çV[`@Q€‘\u0003¡²Þ/¾€\u001a\röÀËÝýD‹£Ä\u001dH @Ê5Ål–ï\u000fÊç!¨‚`@Qa\u000cP‘a\u0015\u001fV[`\u0000€`\u0001[ƒQ\u0010\u0015a\u000c‹W„‚Q\u0010a\r“Wa\r“a\u0013œV[` \u0002` \u0001\u0001Q\u0011\u0015a\r¾WƒQ\u0010a\r³Wa\r³a\u0013œV[` \u0002` \u0001\u0001Q‘P[€a\rȁa\u0013LV[‘PPa\rwV[`\u0000€€[ƒQ\u0010\u0015a\u000c‹W„‚Q\u0010a\rñWa\rña\u0013œV[` \u0002` \u0001\u0001Q\u0011\u0015a\u000e\u001cWƒQ\u0010a\u000e\u0011Wa\u000e\u0011a\u0013œV[` \u0002` \u0001\u0001Q‘P[€a\u000e&a\u0013LV[‘PPa\rÕV[`\u0000`\u0002[‚\u0010\u0015a\t’Wa\u000eE„a\u0012÷V[\u0015a\u000eSWP`\u0000’‘PPV[€a\u000e]a\u0013LV[‘PPa\u000e3V[`\u0000€€[ƒ\u0011a\u000c‹Wa\u000e{ƒa\u0013eV[‘P€a\u000e‡a\u0013LV[‘PPa\u000ejV[```\u0001‚Q\u0011a\u000ežWPV[a\u000e·‚`\u0000`\u0001…Qa\u000e²‘a\u0013!V[a\u0010CV[PV[`\u0000€[‚\u0010\u0015a\nQWa\u000eсa\u0013LV[’PPa\u000e݂a\tJV[\u0015a\u000eðW€a\u000eìa\u0013LV[‘PP[a\u000e¿V[```\u0001‚Q\u0011a\u000f\u0004WPV[a\u000e·‚`\u0001€…Qa\u000e²‘a\u0013!V[sq\tpžÏ©\u001a€boó˜hö[\u001dÑ-;\u0015a\u0010\u0012W`@€Qsq\tpžÏ©\u001a€boó˜hö[\u001dÑ-` ‚\u0001Re\u0019˜Z[\u0019Y`Ò\u001b’‚\u0001’’R`\u0001``‚\u0001R`\u0000‘pÊ\u0010»ÐÛý ©ô±4\u0002Ál± p^\r\u001c\nê±\u000f£S®XoĐ`€\u0001`@€Q`\u001f\u0019„\u0003\u0001R‚Ra\u000f±’‘` \u0001a\u0013ÞV[`@€Q`\u001f\u0019„\u0003\u0001R‚Ra\u000fˑa\u0014\u000fV[`\u0000`@Q€ƒ\u0003`\u0000†Zñ‘PP=€`\u0000\u0014a\u0010\u0008W`@Q‘P`\u001f\u0019`?=\u0001\u0016‚\u0001`@R=‚R=`\u0000` „\u0001>a\u0010\rV[``‘P[PPPP[`\u0000€Taÿ\u0000\u0019\u0016a\u0001\u0000\u0017UV[`\u0000a\u00101`\u0002‚a\u00138V[a\nwg\rඳ§d\u0000\u0000†a\u0013}V[€‚\u0010a\u0010OWPPPV[`\u0000…`\u0002a\u0010`……a\u0013!V[a\u0010j‘a\u00138V[a\u0010t‡a\u0013eV[Q\u0010a\u0010„Wa\u0010„a\u0013œV[` \u0002` \u0001\u0001QP[ƒ\u0011a\u0011¤W[€†„Q\u0010a\u0010ªWa\u0010ªa\u0013œV[` \u0002` \u0001\u0001Q\u0010\u0015a\u0010ÊW‚a\u0010a\u0013LV[“PPa\u0010—V[…‚Q\u0010a\u0010ÜWa\u0010Üa\u0013œV[` \u0002` \u0001\u0001Q\u0010€\u0015a\u0010òWP`\u0000‚\u0011[\u0015a\u0011\tWa\u0011\u0001a\u0015IV[’PPa\u0010ÊV[ƒ\u0011a\u0011ŸW…‚Q\u0010a\u0011\"Wa\u0011\"a\u0013œV[` \u0002` \u0001\u0001Q†„Q\u0010a\u0011=`\u0000ý[PPPP`\u0000`\u0002‚`\u0001a\u0004‘a\u0013eV[a\u0004™„a\u0013}V[a\u0004£‘a\u00138V[P`\u0000a\u0004°ƒa\u000c`V[Pa\u0003\u0014‚‚a\u000c’V[`\u0000a\u0004ǂa\rqV[P`\u0001`\u0000[ƒQ\u0010€\u0015a\u0004ÛWP[\u0015a\u0005\u0012WƒQ\u0010a\u0004òWa\u0004òa\u0013œV[` \u0002` \u0001\u0001Qƒ\u0010\u0015‘P€€a\u0005\na\u0013LV[‘PPa\u0004ÎV[Pa\u0003\u0014a\t›V[`\u0000a\u0003&`da\u0005‰V[`\u0000a\u00053‚a\rÐV[P`\u0001`\u0000[ƒQ\u0010€\u0015a\u0005GWP[\u0015a\u0005\u0012WƒQ\u0010a\u0005^Wa\u0005^a\u0013œV[` \u0002` \u0001\u0001Qƒ\u0010\u0015‘P€€a\u0005va\u0013LV[‘PPa\u0005:V[`\u0000a\u0002˃a\u000e.V[`@Qc&1ò±`á\u001bRf¸\u0017\u0002à\\\u000bo‚\u0011\u0015`\u0004‚\u0001R`\u0000sq\tpžÏ©\u001a€boó˜hö[\u001dÑ-cLcåb`$\u0001`\u0000`@Q€ƒ\u0003`\u0000‡€;\u0015€\u0015a\u0005âW`\u0000€ý[PZñ\u0015€\u0015a\u0005öW=`\u0000€>=`\u0000ý[PPPP`\u0000[‚\u0015a\u0006!Wa\u0006\rƒ‚a\u0013eV[Pa\u0006\u001a`\u0001„a\u0013!V[’Pa\u0005ýV[’‘PPV[`@Qc&1ò±`á\u001bR`d‚\u0011\u0015`\u0004‚\u0001Rsq\tpžÏ©\u001a€boó˜hö[\u001dÑ-cLcåb`$\u0001`\u0000`@Q€ƒ\u0003`\u0000‡€;\u0015€\u0015a\u0006wW`\u0000€ý[PZñ\u0015€\u0015a\u0006‹W=`\u0000€>=`\u0000ý[PPPP`\u0000`\u0002‚`\u0001a\u0006 ‘a\u0013eV[a\u0006ª„a\u0013}V[a\u0006´‘a\u00138V[P`\u0000a\u0004°ƒa\u000eeV[`\u0000a\u0006̂a\u000eV[P`\u0001€[‚Q\u0010€\u0015a\u0006ßWP[\u0015a\u0005\u0012WƒQ\u0010a\u0006öWa\u0006öa\u0013œV[` \u0002` \u0001\u0001Q„`\u0001ƒa\u0007\u000c‘a\u0013!V[Q\u0010a\u0007\u001cWa\u0007\u001ca\u0013œV[` \u0002` \u0001\u0001Q\u0011\u0015‘P€€a\u00073a\u0013LV[‘PPa\u0006ÒV[`\u0000a\u0007Fƒa\u000e»V[P‚`\u0000\u0003a\u0007[Wa\u0003\u0014`\u0000a\u000c’V[a\u0007ga\u0002݂a\tJV[`\u0000a\u0007|a\u0007w`\u0001†a\u0013!V[a\u000e»V[Pa\u0003ƒ„\u0011\u0015€a\u0007WP‚„\u0010\u0015[€a\u0002ÝWPa\u0007Ÿ„a\tJV[\u0015a\t›V[`\u0000€Ta\u0001\u0000\u0004`ÿ\u0016\u0015a\u0007ÅWP`\u0000Ta\u0001\u0000\u0004`ÿ\u0016V[`\u0000sq\tpžÏ©\u001a€boó˜hö[\u001dÑ-;\u0015a\u0008ËW`@€Qsq\tpžÏ©\u001a€boó˜hö[\u001dÑ-` ‚\u0001Re\u0019˜Z[\u0019Y`Ò\u001b‚„\u0001R‚Q€ƒ\u0003„\u0001R``ƒ\u0001“R`\u0000’‘a\u0008S‘fpÊA\u001dpêÕ\r\\\"\u0007\r¯Ãj×_=Ï^r7²*ޚìđ`€\u0001a\u0013ÞV[`@€Q`\u001f\u0019„\u0003\u0001R‚Ra\u0008m‘a\u0014\u000fV[`\u0000`@Q€ƒ\u0003`\u0000†Zñ‘PP=€`\u0000\u0014a\u0008ªW`@Q‘P`\u001f\u0019`?=\u0001\u0016‚\u0001`@R=‚R=`\u0000` „\u0001>a\u0008¯V[``‘P[P‘PP€€` \u0001Q\u0001a\u0008Ǒa\u0014+V[‘PP[‘PV[`\u0000a\u0008ۂa\u000eõV[P`\u0001€[‚Q\u0010€\u0015a\u0008îWP[\u0015a\u0005\u0012WƒQ\u0010a\t\u0005Wa\t\u0005a\u0013œV[` \u0002` \u0001\u0001Q„`\u0001ƒa\t\u001b‘a\u0013!V[Q\u0010a\t+Wa\t+a\u0013œV[` \u0002` \u0001\u0001Q\u0011\u0015‘P€€a\tBa\u0013LV[‘PPa\u0008áV[`\u0000`\u0002‚\u0010\u0015a\t]WP`\u0000‘PV[`\u0002[‚\u0010\u0015a\t’Wa\tr„a\u0012÷V[\u0015a\t€WP`\u0000’‘PPV[€a\tŠa\u0013LV[‘PPa\t`V[P`\u0001’‘PPV[€a\u0003£WA0O¬Ù2=u±\u001bÍÖ\tË8ïÿý°W\u0010÷Êðé±lmpŸP`@Qa\tÿ` €‚R`\u0017‚\u0001RError: Assertion Failed\u0000\u0000\u0000\u0000\u0000\u0000\u0000\u0000\u0000`@‚\u0001R``\u0001V[`@Q€‘\u0003¡a\u0003£a\u000f\u0017V[`\u0000`\u0000\u0003a\n!WP`\u0000‘PV[[€‘P`\u0002a\n3…„a\u0010#V[a\n=‘a\u0013eV[a\nG‘a\u00138V[P\u0003a\n#W[P‘PV[`\u0000g\rඳ§d\u0000\u0000a\nm`\u0002‚a\u00138V[a\nw„†a\u0013}V[a\n‘a\u0013eV[a\n‹‘a\u00138V[“’PPPV[`\u0000`\u0002‚\u0010\u0015a\n¥WP`\u0000‘PV[`\u0002[a\n³`\u0002„a\u00138V[\u0011a\t’Wa\nÁ„a\u0012÷V[\u0015a\nÑWP`\u0000’‘PPV[€a\nہa\u0013LV[‘PPa\n¨V[€\u0015\u0015‚\u0015\u0015\u0014a\u0004\u0006WA0O¬Ù2=u±\u001bÍÖ\tË8ïÿý°W\u0010÷Êðé±lmpŸP`@Qa\u000bX` €‚R`\"‚\u0001RError: a == b not satisfied [boo`@‚\u0001Ral]`ð\u001b``‚\u0001R`€\u0001V[`@Q€‘\u0003¡(\u000fDF²Š\u0013rA}Úe0¹[)’±*ÉÇóxS_)©zÏ5ƒa\u000b©W`@Q€`@\u0001`@R€`\u0005R` \u0001dfalse`Ø\u001bRPa\u000bÇV[`@Q€`@\u0001`@R€`\u0004R` \u0001ctrue`à\u001bRP[`@Qa\u000bԑa\u0014yV[`@Q€‘\u0003¡(\u000fDF²Š\u0013rA}Úe0¹[)’±*ÉÇóxS_)©zÏ5ƒ‚a\u000c%W`@Q€`@\u0001`@R€`\u0005R` \u0001dfalse`Ø\u001bRPa\u000cCV[`@Q€`@\u0001`@R€`\u0004R` \u0001ctrue`à\u001bRP[`@Qa\u000cP‘a\u0014½V[`@Q€‘\u0003¡a\u0004\u0006a\u000f\u0017V[`\u0000€€[ƒ\u0010\u0015a\u000c‹Wa\u000cwƒa\u0013eV[‘P€a\u000cƒa\u0013LV[‘PPa\u000ceV[P’‘PPV[€‚\u0014a\u0004\u0006WA0O¬Ù2=u±\u001bÍÖ\tË8ïÿý°W\u0010÷Êðé±lmpŸP`@Qa\r\u0003` €‚R`\"‚\u0001RError: a == b not satisfied [uin`@‚\u0001Rat]`ð\u001b``‚\u0001R`€\u0001V[`@Q€‘\u0003¡²Þ/¾€\u001a\röÀËÝýD‹£Ä\u001dH @Ê5Ål–ï\u000fÊç!¨`@Qa\r:‘a\u0014çV[`@Q€‘\u0003¡²Þ/¾€\u001a\röÀËÝýD‹£Ä\u001dH @Ê5Ål–ï\u000fÊç!¨‚`@Qa\u000cP‘a\u0015\u001fV[`\u0000€`\u0001[ƒQ\u0010\u0015a\u000c‹W„‚Q\u0010a\r“Wa\r“a\u0013œV[` \u0002` \u0001\u0001Q\u0011\u0015a\r¾WƒQ\u0010a\r³Wa\r³a\u0013œV[` \u0002` \u0001\u0001Q‘P[€a\rȁa\u0013LV[‘PPa\rwV[`\u0000€€[ƒQ\u0010\u0015a\u000c‹W„‚Q\u0010a\rñWa\rña\u0013œV[` \u0002` \u0001\u0001Q\u0011\u0015a\u000e\u001cWƒQ\u0010a\u000e\u0011Wa\u000e\u0011a\u0013œV[` \u0002` \u0001\u0001Q‘P[€a\u000e&a\u0013LV[‘PPa\rÕV[`\u0000`\u0002[‚\u0010\u0015a\t’Wa\u000eE„a\u0012÷V[\u0015a\u000eSWP`\u0000’‘PPV[€a\u000e]a\u0013LV[‘PPa\u000e3V[`\u0000€€[ƒ\u0011a\u000c‹Wa\u000e{ƒa\u0013eV[‘P€a\u000e‡a\u0013LV[‘PPa\u000ejV[```\u0001‚Q\u0011a\u000ežWPV[a\u000e·‚`\u0000`\u0001…Qa\u000e²‘a\u0013!V[a\u0010CV[PV[`\u0000€[‚\u0010\u0015a\nQWa\u000eсa\u0013LV[’PPa\u000e݂a\tJV[\u0015a\u000eðW€a\u000eìa\u0013LV[‘PP[a\u000e¿V[```\u0001‚Q\u0011a\u000f\u0004WPV[a\u000e·‚`\u0001€…Qa\u000e²‘a\u0013!V[sq\tpžÏ©\u001a€boó˜hö[\u001dÑ-;\u0015a\u0010\u0012W`@€Qsq\tpžÏ©\u001a€boó˜hö[\u001dÑ-` ‚\u0001Re\u0019˜Z[\u0019Y`Ò\u001b’‚\u0001’’R`\u0001``‚\u0001R`\u0000‘pÊ\u0010»ÐÛý ©ô±4\u0002Ál± p^\r\u001c\nê±\u000f£S®XoĐ`€\u0001`@€Q`\u001f\u0019„\u0003\u0001R‚Ra\u000f±’‘` \u0001a\u0013ÞV[`@€Q`\u001f\u0019„\u0003\u0001R‚Ra\u000fˑa\u0014\u000fV[`\u0000`@Q€ƒ\u0003`\u0000†Zñ‘PP=€`\u0000\u0014a\u0010\u0008W`@Q‘P`\u001f\u0019`?=\u0001\u0016‚\u0001`@R=‚R=`\u0000` „\u0001>a\u0010\rV[``‘P[PPPP[`\u0000€Taÿ\u0000\u0019\u0016a\u0001\u0000\u0017UV[`\u0000a\u00101`\u0002‚a\u00138V[a\nwg\rඳ§d\u0000\u0000†a\u0013}V[€‚\u0010a\u0010OWPPPV[`\u0000…`\u0002a\u0010`……a\u0013!V[a\u0010j‘a\u00138V[a\u0010t‡a\u0013eV[Q\u0010a\u0010„Wa\u0010„a\u0013œV[` \u0002` \u0001\u0001QP[ƒ\u0011a\u0011¤W[€†„Q\u0010a\u0010ªWa\u0010ªa\u0013œV[` \u0002` \u0001\u0001Q\u0010\u0015a\u0010ÊW‚a\u0010a\u0013LV[“PPa\u0010—V[…‚Q\u0010a\u0010ÜWa\u0010Üa\u0013œV[` \u0002` \u0001\u0001Q\u0010€\u0015a\u0010òWP`\u0000‚\u0011[\u0015a\u0011\tWa\u0011\u0001a\u0015IV[’PPa\u0010ÊV[ƒ\u0011a\u0011ŸW…‚Q\u0010a\u0011\"Wa\u0011\"a\u0013œV[` \u0002` \u0001\u0001Q†„Q\u0010a\u0011=`\u0000ý[PPPP`\u0000`\u0002‚`\u0001a\u0004‘a\u0013eV[a\u0004™„a\u0013}V[a\u0004£‘a\u00138V[P`\u0000a\u0004°ƒa\u000c`V[Pa\u0003\u0014‚‚a\u000c’V[`\u0000a\u0004ǂa\rqV[P`\u0001`\u0000[ƒQ\u0010€\u0015a\u0004ÛWP[\u0015a\u0005\u0012WƒQ\u0010a\u0004òWa\u0004òa\u0013œV[` \u0002` \u0001\u0001Qƒ\u0010\u0015‘P€€a\u0005\na\u0013LV[‘PPa\u0004ÎV[Pa\u0003\u0014a\t›V[`\u0000a\u0003&`da\u0005‰V[`\u0000a\u00053‚a\rÐV[P`\u0001`\u0000[ƒQ\u0010€\u0015a\u0005GWP[\u0015a\u0005\u0012WƒQ\u0010a\u0005^Wa\u0005^a\u0013œV[` \u0002` \u0001\u0001Qƒ\u0010\u0015‘P€€a\u0005va\u0013LV[‘PPa\u0005:V[`\u0000a\u0002˃a\u000e.V[`@Qc&1ò±`á\u001bRf¸\u0017\u0002à\\\u000bo‚\u0011\u0015`\u0004‚\u0001R`\u0000sq\tpžÏ©\u001a€boó˜hö[\u001dÑ-cLcåb`$\u0001`\u0000`@Q€ƒ\u0003`\u0000‡€;\u0015€\u0015a\u0005âW`\u0000€ý[PZñ\u0015€\u0015a\u0005öW=`\u0000€>=`\u0000ý[PPPP`\u0000[‚\u0015a\u0006!Wa\u0006\rƒ‚a\u0013eV[Pa\u0006\u001a`\u0001„a\u0013!V[’Pa\u0005ýV[’‘PPV[`@Qc&1ò±`á\u001bR`d‚\u0011\u0015`\u0004‚\u0001Rsq\tpžÏ©\u001a€boó˜hö[\u001dÑ-cLcåb`$\u0001`\u0000`@Q€ƒ\u0003`\u0000‡€;\u0015€\u0015a\u0006wW`\u0000€ý[PZñ\u0015€\u0015a\u0006‹W=`\u0000€>=`\u0000ý[PPPP`\u0000`\u0002‚`\u0001a\u0006 ‘a\u0013eV[a\u0006ª„a\u0013}V[a\u0006´‘a\u00138V[P`\u0000a\u0004°ƒa\u000eeV[`\u0000a\u0006̂a\u000eV[P`\u0001€[‚Q\u0010€\u0015a\u0006ßWP[\u0015a\u0005\u0012WƒQ\u0010a\u0006öWa\u0006öa\u0013œV[` \u0002` \u0001\u0001Q„`\u0001ƒa\u0007\u000c‘a\u0013!V[Q\u0010a\u0007\u001cWa\u0007\u001ca\u0013œV[` \u0002` \u0001\u0001Q\u0011\u0015‘P€€a\u00073a\u0013LV[‘PPa\u0006ÒV[`\u0000a\u0007Fƒa\u000e»V[P‚`\u0000\u0003a\u0007[Wa\u0003\u0014`\u0000a\u000c’V[a\u0007ga\u0002݂a\tJV[`\u0000a\u0007|a\u0007w`\u0001†a\u0013!V[a\u000e»V[Pa\u0003ƒ„\u0011\u0015€a\u0007WP‚„\u0010\u0015[€a\u0002ÝWPa\u0007Ÿ„a\tJV[\u0015a\t›V[`\u0000€Ta\u0001\u0000\u0004`ÿ\u0016\u0015a\u0007ÅWP`\u0000Ta\u0001\u0000\u0004`ÿ\u0016V[`\u0000sq\tpžÏ©\u001a€boó˜hö[\u001dÑ-;\u0015a\u0008ËW`@€Qsq\tpžÏ©\u001a€boó˜hö[\u001dÑ-` ‚\u0001Re\u0019˜Z[\u0019Y`Ò\u001b‚„\u0001R‚Q€ƒ\u0003„\u0001R``ƒ\u0001“R`\u0000’‘a\u0008S‘fpÊA\u001dpêÕ\r\\\"\u0007\r¯Ãj×_=Ï^r7²*ޚìđ`€\u0001a\u0013ÞV[`@€Q`\u001f\u0019„\u0003\u0001R‚Ra\u0008m‘a\u0014\u000fV[`\u0000`@Q€ƒ\u0003`\u0000†Zñ‘PP=€`\u0000\u0014a\u0008ªW`@Q‘P`\u001f\u0019`?=\u0001\u0016‚\u0001`@R=‚R=`\u0000` „\u0001>a\u0008¯V[``‘P[P‘PP€€` \u0001Q\u0001a\u0008Ǒa\u0014+V[‘PP[‘PV[`\u0000a\u0008ۂa\u000eõV[P`\u0001€[‚Q\u0010€\u0015a\u0008îWP[\u0015a\u0005\u0012WƒQ\u0010a\t\u0005Wa\t\u0005a\u0013œV[` \u0002` \u0001\u0001Q„`\u0001ƒa\t\u001b‘a\u0013!V[Q\u0010a\t+Wa\t+a\u0013œV[` \u0002` \u0001\u0001Q\u0011\u0015‘P€€a\tBa\u0013LV[‘PPa\u0008áV[`\u0000`\u0002‚\u0010\u0015a\t]WP`\u0000‘PV[`\u0002[‚\u0010\u0015a\t’Wa\tr„a\u0012÷V[\u0015a\t€WP`\u0000’‘PPV[€a\tŠa\u0013LV[‘PPa\t`V[P`\u0001’‘PPV[€a\u0003£WA0O¬Ù2=u±\u001bÍÖ\tË8ïÿý°W\u0010÷Êðé±lmpŸP`@Qa\tÿ` €‚R`\u0017‚\u0001RError: Assertion Failed\u0000\u0000\u0000\u0000\u0000\u0000\u0000\u0000\u0000`@‚\u0001R``\u0001V[`@Q€‘\u0003¡a\u0003£a\u000f\u0017V[`\u0000`\u0000\u0003a\n!WP`\u0000‘PV[[€‘P`\u0002a\n3…„a\u0010#V[a\n=‘a\u0013eV[a\nG‘a\u00138V[P\u0003a\n#W[P‘PV[`\u0000g\rඳ§d\u0000\u0000a\nm`\u0002‚a\u00138V[a\nw„†a\u0013}V[a\n‘a\u0013eV[a\n‹‘a\u00138V[“’PPPV[`\u0000`\u0002‚\u0010\u0015a\n¥WP`\u0000‘PV[`\u0002[a\n³`\u0002„a\u00138V[\u0011a\t’Wa\nÁ„a\u0012÷V[\u0015a\nÑWP`\u0000’‘PPV[€a\nہa\u0013LV[‘PPa\n¨V[€\u0015\u0015‚\u0015\u0015\u0014a\u0004\u0006WA0O¬Ù2=u±\u001bÍÖ\tË8ïÿý°W\u0010÷Êðé±lmpŸP`@Qa\u000bX` €‚R`\"‚\u0001RError: a == b not satisfied [boo`@‚\u0001Ral]`ð\u001b``‚\u0001R`€\u0001V[`@Q€‘\u0003¡(\u000fDF²Š\u0013rA}Úe0¹[)’±*ÉÇóxS_)©zÏ5ƒa\u000b©W`@Q€`@\u0001`@R€`\u0005R` \u0001dfalse`Ø\u001bRPa\u000bÇV[`@Q€`@\u0001`@R€`\u0004R` \u0001ctrue`à\u001bRP[`@Qa\u000bԑa\u0014yV[`@Q€‘\u0003¡(\u000fDF²Š\u0013rA}Úe0¹[)’±*ÉÇóxS_)©zÏ5ƒ‚a\u000c%W`@Q€`@\u0001`@R€`\u0005R` \u0001dfalse`Ø\u001bRPa\u000cCV[`@Q€`@\u0001`@R€`\u0004R` \u0001ctrue`à\u001bRP[`@Qa\u000cP‘a\u0014½V[`@Q€‘\u0003¡a\u0004\u0006a\u000f\u0017V[`\u0000€€[ƒ\u0010\u0015a\u000c‹Wa\u000cwƒa\u0013eV[‘P€a\u000cƒa\u0013LV[‘PPa\u000ceV[P’‘PPV[€‚\u0014a\u0004\u0006WA0O¬Ù2=u±\u001bÍÖ\tË8ïÿý°W\u0010÷Êðé±lmpŸP`@Qa\r\u0003` €‚R`\"‚\u0001RError: a == b not satisfied [uin`@‚\u0001Rat]`ð\u001b``‚\u0001R`€\u0001V[`@Q€‘\u0003¡²Þ/¾€\u001a\röÀËÝýD‹£Ä\u001dH @Ê5Ål–ï\u000fÊç!¨`@Qa\r:‘a\u0014çV[`@Q€‘\u0003¡²Þ/¾€\u001a\röÀËÝýD‹£Ä\u001dH @Ê5Ål–ï\u000fÊç!¨‚`@Qa\u000cP‘a\u0015\u001fV[`\u0000€`\u0001[ƒQ\u0010\u0015a\u000c‹W„‚Q\u0010a\r“Wa\r“a\u0013œV[` \u0002` \u0001\u0001Q\u0011\u0015a\r¾WƒQ\u0010a\r³Wa\r³a\u0013œV[` \u0002` \u0001\u0001Q‘P[€a\rȁa\u0013LV[‘PPa\rwV[`\u0000€€[ƒQ\u0010\u0015a\u000c‹W„‚Q\u0010a\rñWa\rña\u0013œV[` \u0002` \u0001\u0001Q\u0011\u0015a\u000e\u001cWƒQ\u0010a\u000e\u0011Wa\u000e\u0011a\u0013œV[` \u0002` \u0001\u0001Q‘P[€a\u000e&a\u0013LV[‘PPa\rÕV[`\u0000`\u0002[‚\u0010\u0015a\t’Wa\u000eE„a\u0012÷V[\u0015a\u000eSWP`\u0000’‘PPV[€a\u000e]a\u0013LV[‘PPa\u000e3V[`\u0000€€[ƒ\u0011a\u000c‹Wa\u000e{ƒa\u0013eV[‘P€a\u000e‡a\u0013LV[‘PPa\u000ejV[```\u0001‚Q\u0011a\u000ežWPV[a\u000e·‚`\u0000`\u0001…Qa\u000e²‘a\u0013!V[a\u0010CV[PV[`\u0000€[‚\u0010\u0015a\nQWa\u000eсa\u0013LV[’PPa\u000e݂a\tJV[\u0015a\u000eðW€a\u000eìa\u0013LV[‘PP[a\u000e¿V[```\u0001‚Q\u0011a\u000f\u0004WPV[a\u000e·‚`\u0001€…Qa\u000e²‘a\u0013!V[sq\tpžÏ©\u001a€boó˜hö[\u001dÑ-;\u0015a\u0010\u0012W`@€Qsq\tpžÏ©\u001a€boó˜hö[\u001dÑ-` ‚\u0001Re\u0019˜Z[\u0019Y`Ò\u001b’‚\u0001’’R`\u0001``‚\u0001R`\u0000‘pÊ\u0010»ÐÛý ©ô±4\u0002Ál± p^\r\u001c\nê±\u000f£S®XoĐ`€\u0001`@€Q`\u001f\u0019„\u0003\u0001R‚Ra\u000f±’‘` \u0001a\u0013ÞV[`@€Q`\u001f\u0019„\u0003\u0001R‚Ra\u000fˑa\u0014\u000fV[`\u0000`@Q€ƒ\u0003`\u0000†Zñ‘PP=€`\u0000\u0014a\u0010\u0008W`@Q‘P`\u001f\u0019`?=\u0001\u0016‚\u0001`@R=‚R=`\u0000` „\u0001>a\u0010\rV[``‘P[PPPP[`\u0000€Taÿ\u0000\u0019\u0016a\u0001\u0000\u0017UV[`\u0000a\u00101`\u0002‚a\u00138V[a\nwg\rඳ§d\u0000\u0000†a\u0013}V[€‚\u0010a\u0010OWPPPV[`\u0000…`\u0002a\u0010`……a\u0013!V[a\u0010j‘a\u00138V[a\u0010t‡a\u0013eV[Q\u0010a\u0010„Wa\u0010„a\u0013œV[` \u0002` \u0001\u0001QP[ƒ\u0011a\u0011¤W[€†„Q\u0010a\u0010ªWa\u0010ªa\u0013œV[` \u0002` \u0001\u0001Q\u0010\u0015a\u0010ÊW‚a\u0010a\u0013LV[“PPa\u0010—V[…‚Q\u0010a\u0010ÜWa\u0010Üa\u0013œV[` \u0002` \u0001\u0001Q\u0010€\u0015a\u0010òWP`\u0000‚\u0011[\u0015a\u0011\tWa\u0011\u0001a\u0015IV[’PPa\u0010ÊV[ƒ\u0011a\u0011ŸW…‚Q\u0010a\u0011\"Wa\u0011\"a\u0013œV[` \u0002` \u0001\u0001Q†„Q\u0010a\u0011=`\u0000ý[PPPP`\u0000`\u0002‚`\u0001a\u0004‘a\u0013eV[a\u0004™„a\u0013}V[a\u0004£‘a\u00138V[P`\u0000a\u0004°ƒa\u000c`V[Pa\u0003\u0014‚‚a\u000c’V[`\u0000a\u0004ǂa\rqV[P`\u0001`\u0000[ƒQ\u0010€\u0015a\u0004ÛWP[\u0015a\u0005\u0012WƒQ\u0010a\u0004òWa\u0004òa\u0013œV[` \u0002` \u0001\u0001Qƒ\u0010\u0015‘P€€a\u0005\na\u0013LV[‘PPa\u0004ÎV[Pa\u0003\u0014a\t›V[`\u0000a\u0003&`da\u0005‰V[`\u0000a\u00053‚a\rÐV[P`\u0001`\u0000[ƒQ\u0010€\u0015a\u0005GWP[\u0015a\u0005\u0012WƒQ\u0010a\u0005^Wa\u0005^a\u0013œV[` \u0002` \u0001\u0001Qƒ\u0010\u0015‘P€€a\u0005va\u0013LV[‘PPa\u0005:V[`\u0000a\u0002˃a\u000e.V[`@Qc&1ò±`á\u001bRf¸\u0017\u0002à\\\u000bo‚\u0011\u0015`\u0004‚\u0001R`\u0000sq\tpžÏ©\u001a€boó˜hö[\u001dÑ-cLcåb`$\u0001`\u0000`@Q€ƒ\u0003`\u0000‡€;\u0015€\u0015a\u0005âW`\u0000€ý[PZñ\u0015€\u0015a\u0005öW=`\u0000€>=`\u0000ý[PPPP`\u0000[‚\u0015a\u0006!Wa\u0006\rƒ‚a\u0013eV[Pa\u0006\u001a`\u0001„a\u0013!V[’Pa\u0005ýV[’‘PPV[`@Qc&1ò±`á\u001bR`d‚\u0011\u0015`\u0004‚\u0001Rsq\tpžÏ©\u001a€boó˜hö[\u001dÑ-cLcåb`$\u0001`\u0000`@Q€ƒ\u0003`\u0000‡€;\u0015€\u0015a\u0006wW`\u0000€ý[PZñ\u0015€\u0015a\u0006‹W=`\u0000€>=`\u0000ý[PPPP`\u0000`\u0002‚`\u0001a\u0006 ‘a\u0013eV[a\u0006ª„a\u0013}V[a\u0006´‘a\u00138V[P`\u0000a\u0004°ƒa\u000eeV[`\u0000a\u0006̂a\u000eV[P`\u0001€[‚Q\u0010€\u0015a\u0006ßWP[\u0015a\u0005\u0012WƒQ\u0010a\u0006öWa\u0006öa\u0013œV[` \u0002` \u0001\u0001Q„`\u0001ƒa\u0007\u000c‘a\u0013!V[Q\u0010a\u0007\u001cWa\u0007\u001ca\u0013œV[` \u0002` \u0001\u0001Q\u0011\u0015‘P€€a\u00073a\u0013LV[‘PPa\u0006ÒV[`\u0000a\u0007Fƒa\u000e»V[P‚`\u0000\u0003a\u0007[Wa\u0003\u0014`\u0000a\u000c’V[a\u0007ga\u0002݂a\tJV[`\u0000a\u0007|a\u0007w`\u0001†a\u0013!V[a\u000e»V[Pa\u0003ƒ„\u0011\u0015€a\u0007WP‚„\u0010\u0015[€a\u0002ÝWPa\u0007Ÿ„a\tJV[\u0015a\t›V[`\u0000€Ta\u0001\u0000\u0004`ÿ\u0016\u0015a\u0007ÅWP`\u0000Ta\u0001\u0000\u0004`ÿ\u0016V[`\u0000sq\tpžÏ©\u001a€boó˜hö[\u001dÑ-;\u0015a\u0008ËW`@€Qsq\tpžÏ©\u001a€boó˜hö[\u001dÑ-` ‚\u0001Re\u0019˜Z[\u0019Y`Ò\u001b‚„\u0001R‚Q€ƒ\u0003„\u0001R``ƒ\u0001“R`\u0000’‘a\u0008S‘fpÊA\u001dpêÕ\r\\\"\u0007\r¯Ãj×_=Ï^r7²*ޚìđ`€\u0001a\u0013ÞV[`@€Q`\u001f\u0019„\u0003\u0001R‚Ra\u0008m‘a\u0014\u000fV[`\u0000`@Q€ƒ\u0003`\u0000†Zñ‘PP=€`\u0000\u0014a\u0008ªW`@Q‘P`\u001f\u0019`?=\u0001\u0016‚\u0001`@R=‚R=`\u0000` „\u0001>a\u0008¯V[``‘P[P‘PP€€` \u0001Q\u0001a\u0008Ǒa\u0014+V[‘PP[‘PV[`\u0000a\u0008ۂa\u000eõV[P`\u0001€[‚Q\u0010€\u0015a\u0008îWP[\u0015a\u0005\u0012WƒQ\u0010a\t\u0005Wa\t\u0005a\u0013œV[` \u0002` \u0001\u0001Q„`\u0001ƒa\t\u001b‘a\u0013!V[Q\u0010a\t+Wa\t+a\u0013œV[` \u0002` \u0001\u0001Q\u0011\u0015‘P€€a\tBa\u0013LV[‘PPa\u0008áV[`\u0000`\u0002‚\u0010\u0015a\t]WP`\u0000‘PV[`\u0002[‚\u0010\u0015a\t’Wa\tr„a\u0012÷V[\u0015a\t€WP`\u0000’‘PPV[€a\tŠa\u0013LV[‘PPa\t`V[P`\u0001’‘PPV[€a\u0003£WA0O¬Ù2=u±\u001bÍÖ\tË8ïÿý°W\u0010÷Êðé±lmpŸP`@Qa\tÿ` €‚R`\u0017‚\u0001RError: Assertion Failed\u0000\u0000\u0000\u0000\u0000\u0000\u0000\u0000\u0000`@‚\u0001R``\u0001V[`@Q€‘\u0003¡a\u0003£a\u000f\u0017V[`\u0000`\u0000\u0003a\n!WP`\u0000‘PV[[€‘P`\u0002a\n3…„a\u0010#V[a\n=‘a\u0013eV[a\nG‘a\u00138V[P\u0003a\n#W[P‘PV[`\u0000g\rඳ§d\u0000\u0000a\nm`\u0002‚a\u00138V[a\nw„†a\u0013}V[a\n‘a\u0013eV[a\n‹‘a\u00138V[“’PPPV[`\u0000`\u0002‚\u0010\u0015a\n¥WP`\u0000‘PV[`\u0002[a\n³`\u0002„a\u00138V[\u0011a\t’Wa\nÁ„a\u0012÷V[\u0015a\nÑWP`\u0000’‘PPV[€a\nہa\u0013LV[‘PPa\n¨V[€\u0015\u0015‚\u0015\u0015\u0014a\u0004\u0006WA0O¬Ù2=u±\u001bÍÖ\tË8ïÿý°W\u0010÷Êðé±lmpŸP`@Qa\u000bX` €‚R`\"‚\u0001RError: a == b not satisfied [boo`@‚\u0001Ral]`ð\u001b``‚\u0001R`€\u0001V[`@Q€‘\u0003¡(\u000fDF²Š\u0013rA}Úe0¹[)’±*ÉÇóxS_)©zÏ5ƒa\u000b©W`@Q€`@\u0001`@R€`\u0005R` \u0001dfalse`Ø\u001bRPa\u000bÇV[`@Q€`@\u0001`@R€`\u0004R` \u0001ctrue`à\u001bRP[`@Qa\u000bԑa\u0014yV[`@Q€‘\u0003¡(\u000fDF²Š\u0013rA}Úe0¹[)’±*ÉÇóxS_)©zÏ5ƒ‚a\u000c%W`@Q€`@\u0001`@R€`\u0005R` \u0001dfalse`Ø\u001bRPa\u000cCV[`@Q€`@\u0001`@R€`\u0004R` \u0001ctrue`à\u001bRP[`@Qa\u000cP‘a\u0014½V[`@Q€‘\u0003¡a\u0004\u0006a\u000f\u0017V[`\u0000€€[ƒ\u0010\u0015a\u000c‹Wa\u000cwƒa\u0013eV[‘P€a\u000cƒa\u0013LV[‘PPa\u000ceV[P’‘PPV[€‚\u0014a\u0004\u0006WA0O¬Ù2=u±\u001bÍÖ\tË8ïÿý°W\u0010÷Êðé±lmpŸP`@Qa\r\u0003` €‚R`\"‚\u0001RError: a == b not satisfied [uin`@‚\u0001Rat]`ð\u001b``‚\u0001R`€\u0001V[`@Q€‘\u0003¡²Þ/¾€\u001a\röÀËÝýD‹£Ä\u001dH @Ê5Ål–ï\u000fÊç!¨`@Qa\r:‘a\u0014çV[`@Q€‘\u0003¡²Þ/¾€\u001a\röÀËÝýD‹£Ä\u001dH @Ê5Ål–ï\u000fÊç!¨‚`@Qa\u000cP‘a\u0015\u001fV[`\u0000€`\u0001[ƒQ\u0010\u0015a\u000c‹W„‚Q\u0010a\r“Wa\r“a\u0013œV[` \u0002` \u0001\u0001Q\u0011\u0015a\r¾WƒQ\u0010a\r³Wa\r³a\u0013œV[` \u0002` \u0001\u0001Q‘P[€a\rȁa\u0013LV[‘PPa\rwV[`\u0000€€[ƒQ\u0010\u0015a\u000c‹W„‚Q\u0010a\rñWa\rña\u0013œV[` \u0002` \u0001\u0001Q\u0011\u0015a\u000e\u001cWƒQ\u0010a\u000e\u0011Wa\u000e\u0011a\u0013œV[` \u0002` \u0001\u0001Q‘P[€a\u000e&a\u0013LV[‘PPa\rÕV[`\u0000`\u0002[‚\u0010\u0015a\t’Wa\u000eE„a\u0012÷V[\u0015a\u000eSWP`\u0000’‘PPV[€a\u000e]a\u0013LV[‘PPa\u000e3V[`\u0000€€[ƒ\u0011a\u000c‹Wa\u000e{ƒa\u0013eV[‘P€a\u000e‡a\u0013LV[‘PPa\u000ejV[```\u0001‚Q\u0011a\u000ežWPV[a\u000e·‚`\u0000`\u0001…Qa\u000e²‘a\u0013!V[a\u0010CV[PV[`\u0000€[‚\u0010\u0015a\nQWa\u000eсa\u0013LV[’PPa\u000e݂a\tJV[\u0015a\u000eðW€a\u000eìa\u0013LV[‘PP[a\u000e¿V[```\u0001‚Q\u0011a\u000f\u0004WPV[a\u000e·‚`\u0001€…Qa\u000e²‘a\u0013!V[sq\tpžÏ©\u001a€boó˜hö[\u001dÑ-;\u0015a\u0010\u0012W`@€Qsq\tpžÏ©\u001a€boó˜hö[\u001dÑ-` ‚\u0001Re\u0019˜Z[\u0019Y`Ò\u001b’‚\u0001’’R`\u0001``‚\u0001R`\u0000‘pÊ\u0010»ÐÛý ©ô±4\u0002Ál± p^\r\u001c\nê±\u000f£S®XoĐ`€\u0001`@€Q`\u001f\u0019„\u0003\u0001R‚Ra\u000f±’‘` \u0001a\u0013ÞV[`@€Q`\u001f\u0019„\u0003\u0001R‚Ra\u000fˑa\u0014\u000fV[`\u0000`@Q€ƒ\u0003`\u0000†Zñ‘PP=€`\u0000\u0014a\u0010\u0008W`@Q‘P`\u001f\u0019`?=\u0001\u0016‚\u0001`@R=‚R=`\u0000` „\u0001>a\u0010\rV[``‘P[PPPP[`\u0000€Taÿ\u0000\u0019\u0016a\u0001\u0000\u0017UV[`\u0000a\u00101`\u0002‚a\u00138V[a\nwg\rඳ§d\u0000\u0000†a\u0013}V[€‚\u0010a\u0010OWPPPV[`\u0000…`\u0002a\u0010`……a\u0013!V[a\u0010j‘a\u00138V[a\u0010t‡a\u0013eV[Q\u0010a\u0010„Wa\u0010„a\u0013œV[` \u0002` \u0001\u0001QP[ƒ\u0011a\u0011¤W[€†„Q\u0010a\u0010ªWa\u0010ªa\u0013œV[` \u0002` \u0001\u0001Q\u0010\u0015a\u0010ÊW‚a\u0010a\u0013LV[“PPa\u0010—V[…‚Q\u0010a\u0010ÜWa\u0010Üa\u0013œV[` \u0002` \u0001\u0001Q\u0010€\u0015a\u0010òWP`\u0000‚\u0011[\u0015a\u0011\tWa\u0011\u0001a\u0015IV[’PPa\u0010ÊV[ƒ\u0011a\u0011ŸW…‚Q\u0010a\u0011\"Wa\u0011\"a\u0013œV[` \u0002` \u0001\u0001Q†„Q\u0010a\u0011=`\u0000ý[PPPP`\u0000`\u0002‚`\u0001a\u0004‘a\u0013eV[a\u0004™„a\u0013}V[a\u0004£‘a\u00138V[P`\u0000a\u0004°ƒa\u000c`V[Pa\u0003\u0014‚‚a\u000c’V[`\u0000a\u0004ǂa\rqV[P`\u0001`\u0000[ƒQ\u0010€\u0015a\u0004ÛWP[\u0015a\u0005\u0012WƒQ\u0010a\u0004òWa\u0004òa\u0013œV[` \u0002` \u0001\u0001Qƒ\u0010\u0015‘P€€a\u0005\na\u0013LV[‘PPa\u0004ÎV[Pa\u0003\u0014a\t›V[`\u0000a\u0003&`da\u0005‰V[`\u0000a\u00053‚a\rÐV[P`\u0001`\u0000[ƒQ\u0010€\u0015a\u0005GWP[\u0015a\u0005\u0012WƒQ\u0010a\u0005^Wa\u0005^a\u0013œV[` \u0002` \u0001\u0001Qƒ\u0010\u0015‘P€€a\u0005va\u0013LV[‘PPa\u0005:V[`\u0000a\u0002˃a\u000e.V[`@Qc&1ò±`á\u001bRf¸\u0017\u0002à\\\u000bo‚\u0011\u0015`\u0004‚\u0001R`\u0000sq\tpžÏ©\u001a€boó˜hö[\u001dÑ-cLcåb`$\u0001`\u0000`@Q€ƒ\u0003`\u0000‡€;\u0015€\u0015a\u0005âW`\u0000€ý[PZñ\u0015€\u0015a\u0005öW=`\u0000€>=`\u0000ý[PPPP`\u0000[‚\u0015a\u0006!Wa\u0006\rƒ‚a\u0013eV[Pa\u0006\u001a`\u0001„a\u0013!V[’Pa\u0005ýV[’‘PPV[`@Qc&1ò±`á\u001bR`d‚\u0011\u0015`\u0004‚\u0001Rsq\tpžÏ©\u001a€boó˜hö[\u001dÑ-cLcåb`$\u0001`\u0000`@Q€ƒ\u0003`\u0000‡€;\u0015€\u0015a\u0006wW`\u0000€ý[PZñ\u0015€\u0015a\u0006‹W=`\u0000€>=`\u0000ý[PPPP`\u0000`\u0002‚`\u0001a\u0006 ‘a\u0013eV[a\u0006ª„a\u0013}V[a\u0006´‘a\u00138V[P`\u0000a\u0004°ƒa\u000eeV[`\u0000a\u0006̂a\u000eV[P`\u0001€[‚Q\u0010€\u0015a\u0006ßWP[\u0015a\u0005\u0012WƒQ\u0010a\u0006öWa\u0006öa\u0013œV[` \u0002` \u0001\u0001Q„`\u0001ƒa\u0007\u000c‘a\u0013!V[Q\u0010a\u0007\u001cWa\u0007\u001ca\u0013œV[` \u0002` \u0001\u0001Q\u0011\u0015‘P€€a\u00073a\u0013LV[‘PPa\u0006ÒV[`\u0000a\u0007Fƒa\u000e»V[P‚`\u0000\u0003a\u0007[Wa\u0003\u0014`\u0000a\u000c’V[a\u0007ga\u0002݂a\tJV[`\u0000a\u0007|a\u0007w`\u0001†a\u0013!V[a\u000e»V[Pa\u0003ƒ„\u0011\u0015€a\u0007WP‚„\u0010\u0015[€a\u0002ÝWPa\u0007Ÿ„a\tJV[\u0015a\t›V[`\u0000€Ta\u0001\u0000\u0004`ÿ\u0016\u0015a\u0007ÅWP`\u0000Ta\u0001\u0000\u0004`ÿ\u0016V[`\u0000sq\tpžÏ©\u001a€boó˜hö[\u001dÑ-;\u0015a\u0008ËW`@€Qsq\tpžÏ©\u001a€boó˜hö[\u001dÑ-` ‚\u0001Re\u0019˜Z[\u0019Y`Ò\u001b‚„\u0001R‚Q€ƒ\u0003„\u0001R``ƒ\u0001“R`\u0000’‘a\u0008S‘fpÊA\u001dpêÕ\r\\\"\u0007\r¯Ãj×_=Ï^r7²*ޚìđ`€\u0001a\u0013ÞV[`@€Q`\u001f\u0019„\u0003\u0001R‚Ra\u0008m‘a\u0014\u000fV[`\u0000`@Q€ƒ\u0003`\u0000†Zñ‘PP=€`\u0000\u0014a\u0008ªW`@Q‘P`\u001f\u0019`?=\u0001\u0016‚\u0001`@R=‚R=`\u0000` „\u0001>a\u0008¯V[``‘P[P‘PP€€` \u0001Q\u0001a\u0008Ǒa\u0014+V[‘PP[‘PV[`\u0000a\u0008ۂa\u000eõV[P`\u0001€[‚Q\u0010€\u0015a\u0008îWP[\u0015a\u0005\u0012WƒQ\u0010a\t\u0005Wa\t\u0005a\u0013œV[` \u0002` \u0001\u0001Q„`\u0001ƒa\t\u001b‘a\u0013!V[Q\u0010a\t+Wa\t+a\u0013œV[` \u0002` \u0001\u0001Q\u0011\u0015‘P€€a\tBa\u0013LV[‘PPa\u0008áV[`\u0000`\u0002‚\u0010\u0015a\t]WP`\u0000‘PV[`\u0002[‚\u0010\u0015a\t’Wa\tr„a\u0012÷V[\u0015a\t€WP`\u0000’‘PPV[€a\tŠa\u0013LV[‘PPa\t`V[P`\u0001’‘PPV[€a\u0003£WA0O¬Ù2=u±\u001bÍÖ\tË8ïÿý°W\u0010÷Êðé±lmpŸP`@Qa\tÿ` €‚R`\u0017‚\u0001RError: Assertion Failed\u0000\u0000\u0000\u0000\u0000\u0000\u0000\u0000\u0000`@‚\u0001R``\u0001V[`@Q€‘\u0003¡a\u0003£a\u000f\u0017V[`\u0000`\u0000\u0003a\n!WP`\u0000‘PV[[€‘P`\u0002a\n3…„a\u0010#V[a\n=‘a\u0013eV[a\nG‘a\u00138V[P\u0003a\n#W[P‘PV[`\u0000g\rඳ§d\u0000\u0000a\nm`\u0002‚a\u00138V[a\nw„†a\u0013}V[a\n‘a\u0013eV[a\n‹‘a\u00138V[“’PPPV[`\u0000`\u0002‚\u0010\u0015a\n¥WP`\u0000‘PV[`\u0002[a\n³`\u0002„a\u00138V[\u0011a\t’Wa\nÁ„a\u0012÷V[\u0015a\nÑWP`\u0000’‘PPV[€a\nہa\u0013LV[‘PPa\n¨V[€\u0015\u0015‚\u0015\u0015\u0014a\u0004\u0006WA0O¬Ù2=u±\u001bÍÖ\tË8ïÿý°W\u0010÷Êðé±lmpŸP`@Qa\u000bX` €‚R`\"‚\u0001RError: a == b not satisfied [boo`@‚\u0001Ral]`ð\u001b``‚\u0001R`€\u0001V[`@Q€‘\u0003¡(\u000fDF²Š\u0013rA}Úe0¹[)’±*ÉÇóxS_)©zÏ5ƒa\u000b©W`@Q€`@\u0001`@R€`\u0005R` \u0001dfalse`Ø\u001bRPa\u000bÇV[`@Q€`@\u0001`@R€`\u0004R` \u0001ctrue`à\u001bRP[`@Qa\u000bԑa\u0014yV[`@Q€‘\u0003¡(\u000fDF²Š\u0013rA}Úe0¹[)’±*ÉÇóxS_)©zÏ5ƒ‚a\u000c%W`@Q€`@\u0001`@R€`\u0005R` \u0001dfalse`Ø\u001bRPa\u000cCV[`@Q€`@\u0001`@R€`\u0004R` \u0001ctrue`à\u001bRP[`@Qa\u000cP‘a\u0014½V[`@Q€‘\u0003¡a\u0004\u0006a\u000f\u0017V[`\u0000€€[ƒ\u0010\u0015a\u000c‹Wa\u000cwƒa\u0013eV[‘P€a\u000cƒa\u0013LV[‘PPa\u000ceV[P’‘PPV[€‚\u0014a\u0004\u0006WA0O¬Ù2=u±\u001bÍÖ\tË8ïÿý°W\u0010÷Êðé±lmpŸP`@Qa\r\u0003` €‚R`\"‚\u0001RError: a == b not satisfied [uin`@‚\u0001Rat]`ð\u001b``‚\u0001R`€\u0001V[`@Q€‘\u0003¡²Þ/¾€\u001a\röÀËÝýD‹£Ä\u001dH @Ê5Ål–ï\u000fÊç!¨`@Qa\r:‘a\u0014çV[`@Q€‘\u0003¡²Þ/¾€\u001a\röÀËÝýD‹£Ä\u001dH @Ê5Ål–ï\u000fÊç!¨‚`@Qa\u000cP‘a\u0015\u001fV[`\u0000€`\u0001[ƒQ\u0010\u0015a\u000c‹W„‚Q\u0010a\r“Wa\r“a\u0013œV[` \u0002` \u0001\u0001Q\u0011\u0015a\r¾WƒQ\u0010a\r³Wa\r³a\u0013œV[` \u0002` \u0001\u0001Q‘P[€a\rȁa\u0013LV[‘PPa\rwV[`\u0000€€[ƒQ\u0010\u0015a\u000c‹W„‚Q\u0010a\rñWa\rña\u0013œV[` \u0002` \u0001\u0001Q\u0011\u0015a\u000e\u001cWƒQ\u0010a\u000e\u0011Wa\u000e\u0011a\u0013œV[` \u0002` \u0001\u0001Q‘P[€a\u000e&a\u0013LV[‘PPa\rÕV[`\u0000`\u0002[‚\u0010\u0015a\t’Wa\u000eE„a\u0012÷V[\u0015a\u000eSWP`\u0000’‘PPV[€a\u000e]a\u0013LV[‘PPa\u000e3V[`\u0000€€[ƒ\u0011a\u000c‹Wa\u000e{ƒa\u0013eV[‘P€a\u000e‡a\u0013LV[‘PPa\u000ejV[```\u0001‚Q\u0011a\u000ežWPV[a\u000e·‚`\u0000`\u0001…Qa\u000e²‘a\u0013!V[a\u0010CV[PV[`\u0000€[‚\u0010\u0015a\nQWa\u000eсa\u0013LV[’PPa\u000e݂a\tJV[\u0015a\u000eðW€a\u000eìa\u0013LV[‘PP[a\u000e¿V[```\u0001‚Q\u0011a\u000f\u0004WPV[a\u000e·‚`\u0001€…Qa\u000e²‘a\u0013!V[sq\tpžÏ©\u001a€boó˜hö[\u001dÑ-;\u0015a\u0010\u0012W`@€Qsq\tpžÏ©\u001a€boó˜hö[\u001dÑ-` ‚\u0001Re\u0019˜Z[\u0019Y`Ò\u001b’‚\u0001’’R`\u0001``‚\u0001R`\u0000‘pÊ\u0010»ÐÛý ©ô±4\u0002Ál± p^\r\u001c\nê±\u000f£S®XoĐ`€\u0001`@€Q`\u001f\u0019„\u0003\u0001R‚Ra\u000f±’‘` \u0001a\u0013ÞV[`@€Q`\u001f\u0019„\u0003\u0001R‚Ra\u000fˑa\u0014\u000fV[`\u0000`@Q€ƒ\u0003`\u0000†Zñ‘PP=€`\u0000\u0014a\u0010\u0008W`@Q‘P`\u001f\u0019`?=\u0001\u0016‚\u0001`@R=‚R=`\u0000` „\u0001>a\u0010\rV[``‘P[PPPP[`\u0000€Taÿ\u0000\u0019\u0016a\u0001\u0000\u0017UV[`\u0000a\u00101`\u0002‚a\u00138V[a\nwg\rඳ§d\u0000\u0000†a\u0013}V[€‚\u0010a\u0010OWPPPV[`\u0000…`\u0002a\u0010`……a\u0013!V[a\u0010j‘a\u00138V[a\u0010t‡a\u0013eV[Q\u0010a\u0010„Wa\u0010„a\u0013œV[` \u0002` \u0001\u0001QP[ƒ\u0011a\u0011¤W[€†„Q\u0010a\u0010ªWa\u0010ªa\u0013œV[` \u0002` \u0001\u0001Q\u0010\u0015a\u0010ÊW‚a\u0010a\u0013LV[“PPa\u0010—V[…‚Q\u0010a\u0010ÜWa\u0010Üa\u0013œV[` \u0002` \u0001\u0001Q\u0010€\u0015a\u0010òWP`\u0000‚\u0011[\u0015a\u0011\tWa\u0011\u0001a\u0015IV[’PPa\u0010ÊV[ƒ\u0011a\u0011ŸW…‚Q\u0010a\u0011\"Wa\u0011\"a\u0013œV[` \u0002` \u0001\u0001Q†„Q\u0010a\u0011=`\u0000ý[PPPP`\u0000`\u0002‚`\u0001a\u0004‘a\u0013eV[a\u0004™„a\u0013}V[a\u0004£‘a\u00138V[P`\u0000a\u0004°ƒa\u000c`V[Pa\u0003\u0014‚‚a\u000c’V[`\u0000a\u0004ǂa\rqV[P`\u0001`\u0000[ƒQ\u0010€\u0015a\u0004ÛWP[\u0015a\u0005\u0012WƒQ\u0010a\u0004òWa\u0004òa\u0013œV[` \u0002` \u0001\u0001Qƒ\u0010\u0015‘P€€a\u0005\na\u0013LV[‘PPa\u0004ÎV[Pa\u0003\u0014a\t›V[`\u0000a\u0003&`da\u0005‰V[`\u0000a\u00053‚a\rÐV[P`\u0001`\u0000[ƒQ\u0010€\u0015a\u0005GWP[\u0015a\u0005\u0012WƒQ\u0010a\u0005^Wa\u0005^a\u0013œV[` \u0002` \u0001\u0001Qƒ\u0010\u0015‘P€€a\u0005va\u0013LV[‘PPa\u0005:V[`\u0000a\u0002˃a\u000e.V[`@Qc&1ò±`á\u001bRf¸\u0017\u0002à\\\u000bo‚\u0011\u0015`\u0004‚\u0001R`\u0000sq\tpžÏ©\u001a€boó˜hö[\u001dÑ-cLcåb`$\u0001`\u0000`@Q€ƒ\u0003`\u0000‡€;\u0015€\u0015a\u0005âW`\u0000€ý[PZñ\u0015€\u0015a\u0005öW=`\u0000€>=`\u0000ý[PPPP`\u0000[‚\u0015a\u0006!Wa\u0006\rƒ‚a\u0013eV[Pa\u0006\u001a`\u0001„a\u0013!V[’Pa\u0005ýV[’‘PPV[`@Qc&1ò±`á\u001bR`d‚\u0011\u0015`\u0004‚\u0001Rsq\tpžÏ©\u001a€boó˜hö[\u001dÑ-cLcåb`$\u0001`\u0000`@Q€ƒ\u0003`\u0000‡€;\u0015€\u0015a\u0006wW`\u0000€ý[PZñ\u0015€\u0015a\u0006‹W=`\u0000€>=`\u0000ý[PPPP`\u0000`\u0002‚`\u0001a\u0006 ‘a\u0013eV[a\u0006ª„a\u0013}V[a\u0006´‘a\u00138V[P`\u0000a\u0004°ƒa\u000eeV[`\u0000a\u0006̂a\u000eV[P`\u0001€[‚Q\u0010€\u0015a\u0006ßWP[\u0015a\u0005\u0012WƒQ\u0010a\u0006öWa\u0006öa\u0013œV[` \u0002` \u0001\u0001Q„`\u0001ƒa\u0007\u000c‘a\u0013!V[Q\u0010a\u0007\u001cWa\u0007\u001ca\u0013œV[` \u0002` \u0001\u0001Q\u0011\u0015‘P€€a\u00073a\u0013LV[‘PPa\u0006ÒV[`\u0000a\u0007Fƒa\u000e»V[P‚`\u0000\u0003a\u0007[Wa\u0003\u0014`\u0000a\u000c’V[a\u0007ga\u0002݂a\tJV[`\u0000a\u0007|a\u0007w`\u0001†a\u0013!V[a\u000e»V[Pa\u0003ƒ„\u0011\u0015€a\u0007WP‚„\u0010\u0015[€a\u0002ÝWPa\u0007Ÿ„a\tJV[\u0015a\t›V[`\u0000€Ta\u0001\u0000\u0004`ÿ\u0016\u0015a\u0007ÅWP`\u0000Ta\u0001\u0000\u0004`ÿ\u0016V[`\u0000sq\tpžÏ©\u001a€boó˜hö[\u001dÑ-;\u0015a\u0008ËW`@€Qsq\tpžÏ©\u001a€boó˜hö[\u001dÑ-` ‚\u0001Re\u0019˜Z[\u0019Y`Ò\u001b‚„\u0001R‚Q€ƒ\u0003„\u0001R``ƒ\u0001“R`\u0000’‘a\u0008S‘fpÊA\u001dpêÕ\r\\\"\u0007\r¯Ãj×_=Ï^r7²*ޚìđ`€\u0001a\u0013ÞV[`@€Q`\u001f\u0019„\u0003\u0001R‚Ra\u0008m‘a\u0014\u000fV[`\u0000`@Q€ƒ\u0003`\u0000†Zñ‘PP=€`\u0000\u0014a\u0008ªW`@Q‘P`\u001f\u0019`?=\u0001\u0016‚\u0001`@R=‚R=`\u0000` „\u0001>a\u0008¯V[``‘P[P‘PP€€` \u0001Q\u0001a\u0008Ǒa\u0014+V[‘PP[‘PV[`\u0000a\u0008ۂa\u000eõV[P`\u0001€[‚Q\u0010€\u0015a\u0008îWP[\u0015a\u0005\u0012WƒQ\u0010a\t\u0005Wa\t\u0005a\u0013œV[` \u0002` \u0001\u0001Q„`\u0001ƒa\t\u001b‘a\u0013!V[Q\u0010a\t+Wa\t+a\u0013œV[` \u0002` \u0001\u0001Q\u0011\u0015‘P€€a\tBa\u0013LV[‘PPa\u0008áV[`\u0000`\u0002‚\u0010\u0015a\t]WP`\u0000‘PV[`\u0002[‚\u0010\u0015a\t’Wa\tr„a\u0012÷V[\u0015a\t€WP`\u0000’‘PPV[€a\tŠa\u0013LV[‘PPa\t`V[P`\u0001’‘PPV[€a\u0003£WA0O¬Ù2=u±\u001bÍÖ\tË8ïÿý°W\u0010÷Êðé±lmpŸP`@Qa\tÿ` €‚R`\u0017‚\u0001RError: Assertion Failed\u0000\u0000\u0000\u0000\u0000\u0000\u0000\u0000\u0000`@‚\u0001R``\u0001V[`@Q€‘\u0003¡a\u0003£a\u000f\u0017V[`\u0000`\u0000\u0003a\n!WP`\u0000‘PV[[€‘P`\u0002a\n3…„a\u0010#V[a\n=‘a\u0013eV[a\nG‘a\u00138V[P\u0003a\n#W[P‘PV[`\u0000g\rඳ§d\u0000\u0000a\nm`\u0002‚a\u00138V[a\nw„†a\u0013}V[a\n‘a\u0013eV[a\n‹‘a\u00138V[“’PPPV[`\u0000`\u0002‚\u0010\u0015a\n¥WP`\u0000‘PV[`\u0002[a\n³`\u0002„a\u00138V[\u0011a\t’Wa\nÁ„a\u0012÷V[\u0015a\nÑWP`\u0000’‘PPV[€a\nہa\u0013LV[‘PPa\n¨V[€\u0015\u0015‚\u0015\u0015\u0014a\u0004\u0006WA0O¬Ù2=u±\u001bÍÖ\tË8ïÿý°W\u0010÷Êðé±lmpŸP`@Qa\u000bX` €‚R`\"‚\u0001RError: a == b not satisfied [boo`@‚\u0001Ral]`ð\u001b``‚\u0001R`€\u0001V[`@Q€‘\u0003¡(\u000fDF²Š\u0013rA}Úe0¹[)’±*ÉÇóxS_)©zÏ5ƒa\u000b©W`@Q€`@\u0001`@R€`\u0005R` \u0001dfalse`Ø\u001bRPa\u000bÇV[`@Q€`@\u0001`@R€`\u0004R` \u0001ctrue`à\u001bRP[`@Qa\u000bԑa\u0014yV[`@Q€‘\u0003¡(\u000fDF²Š\u0013rA}Úe0¹[)’±*ÉÇóxS_)©zÏ5ƒ‚a\u000c%W`@Q€`@\u0001`@R€`\u0005R` \u0001dfalse`Ø\u001bRPa\u000cCV[`@Q€`@\u0001`@R€`\u0004R` \u0001ctrue`à\u001bRP[`@Qa\u000cP‘a\u0014½V[`@Q€‘\u0003¡a\u0004\u0006a\u000f\u0017V[`\u0000€€[ƒ\u0010\u0015a\u000c‹Wa\u000cwƒa\u0013eV[‘P€a\u000cƒa\u0013LV[‘PPa\u000ceV[P’‘PPV[€‚\u0014a\u0004\u0006WA0O¬Ù2=u±\u001bÍÖ\tË8ïÿý°W\u0010÷Êðé±lmpŸP`@Qa\r\u0003` €‚R`\"‚\u0001RError: a == b not satisfied [uin`@‚\u0001Rat]`ð\u001b``‚\u0001R`€\u0001V[`@Q€‘\u0003¡²Þ/¾€\u001a\röÀËÝýD‹£Ä\u001dH @Ê5Ål–ï\u000fÊç!¨`@Qa\r:‘a\u0014çV[`@Q€‘\u0003¡²Þ/¾€\u001a\röÀËÝýD‹£Ä\u001dH @Ê5Ål–ï\u000fÊç!¨‚`@Qa\u000cP‘a\u0015\u001fV[`\u0000€`\u0001[ƒQ\u0010\u0015a\u000c‹W„‚Q\u0010a\r“Wa\r“a\u0013œV[` \u0002` \u0001\u0001Q\u0011\u0015a\r¾WƒQ\u0010a\r³Wa\r³a\u0013œV[` \u0002` \u0001\u0001Q‘P[€a\rȁa\u0013LV[‘PPa\rwV[`\u0000€€[ƒQ\u0010\u0015a\u000c‹W„‚Q\u0010a\rñWa\rña\u0013œV[` \u0002` \u0001\u0001Q\u0011\u0015a\u000e\u001cWƒQ\u0010a\u000e\u0011Wa\u000e\u0011a\u0013œV[` \u0002` \u0001\u0001Q‘P[€a\u000e&a\u0013LV[‘PPa\rÕV[`\u0000`\u0002[‚\u0010\u0015a\t’Wa\u000eE„a\u0012÷V[\u0015a\u000eSWP`\u0000’‘PPV[€a\u000e]a\u0013LV[‘PPa\u000e3V[`\u0000€€[ƒ\u0011a\u000c‹Wa\u000e{ƒa\u0013eV[‘P€a\u000e‡a\u0013LV[‘PPa\u000ejV[```\u0001‚Q\u0011a\u000ežWPV[a\u000e·‚`\u0000`\u0001…Qa\u000e²‘a\u0013!V[a\u0010CV[PV[`\u0000€[‚\u0010\u0015a\nQWa\u000eсa\u0013LV[’PPa\u000e݂a\tJV[\u0015a\u000eðW€a\u000eìa\u0013LV[‘PP[a\u000e¿V[```\u0001‚Q\u0011a\u000f\u0004WPV[a\u000e·‚`\u0001€…Qa\u000e²‘a\u0013!V[sq\tpžÏ©\u001a€boó˜hö[\u001dÑ-;\u0015a\u0010\u0012W`@€Qsq\tpžÏ©\u001a€boó˜hö[\u001dÑ-` ‚\u0001Re\u0019˜Z[\u0019Y`Ò\u001b’‚\u0001’’R`\u0001``‚\u0001R`\u0000‘pÊ\u0010»ÐÛý ©ô±4\u0002Ál± p^\r\u001c\nê±\u000f£S®XoĐ`€\u0001`@€Q`\u001f\u0019„\u0003\u0001R‚Ra\u000f±’‘` \u0001a\u0013ÞV[`@€Q`\u001f\u0019„\u0003\u0001R‚Ra\u000fˑa\u0014\u000fV[`\u0000`@Q€ƒ\u0003`\u0000†Zñ‘PP=€`\u0000\u0014a\u0010\u0008W`@Q‘P`\u001f\u0019`?=\u0001\u0016‚\u0001`@R=‚R=`\u0000` „\u0001>a\u0010\rV[``‘P[PPPP[`\u0000€Taÿ\u0000\u0019\u0016a\u0001\u0000\u0017UV[`\u0000a\u00101`\u0002‚a\u00138V[a\nwg\rඳ§d\u0000\u0000†a\u0013}V[€‚\u0010a\u0010OWPPPV[`\u0000…`\u0002a\u0010`……a\u0013!V[a\u0010j‘a\u00138V[a\u0010t‡a\u0013eV[Q\u0010a\u0010„Wa\u0010„a\u0013œV[` \u0002` \u0001\u0001QP[ƒ\u0011a\u0011¤W[€†„Q\u0010a\u0010ªWa\u0010ªa\u0013œV[` \u0002` \u0001\u0001Q\u0010\u0015a\u0010ÊW‚a\u0010a\u0013LV[“PPa\u0010—V[…‚Q\u0010a\u0010ÜWa\u0010Üa\u0013œV[` \u0002` \u0001\u0001Q\u0010€\u0015a\u0010òWP`\u0000‚\u0011[\u0015a\u0011\tWa\u0011\u0001a\u0015IV[’PPa\u0010ÊV[ƒ\u0011a\u0011ŸW…‚Q\u0010a\u0011\"Wa\u0011\"a\u0013œV[` \u0002` \u0001\u0001Q†„Q\u0010a\u0011=`\u0000ý[PPPP`\u0000`\u0002‚`\u0001a\u0004‘a\u0013eV[a\u0004™„a\u0013}V[a\u0004£‘a\u00138V[P`\u0000a\u0004°ƒa\u000c`V[Pa\u0003\u0014‚‚a\u000c’V[`\u0000a\u0004ǂa\rqV[P`\u0001`\u0000[ƒQ\u0010€\u0015a\u0004ÛWP[\u0015a\u0005\u0012WƒQ\u0010a\u0004òWa\u0004òa\u0013œV[` \u0002` \u0001\u0001Qƒ\u0010\u0015‘P€€a\u0005\na\u0013LV[‘PPa\u0004ÎV[Pa\u0003\u0014a\t›V[`\u0000a\u0003&`da\u0005‰V[`\u0000a\u00053‚a\rÐV[P`\u0001`\u0000[ƒQ\u0010€\u0015a\u0005GWP[\u0015a\u0005\u0012WƒQ\u0010a\u0005^Wa\u0005^a\u0013œV[` \u0002` \u0001\u0001Qƒ\u0010\u0015‘P€€a\u0005va\u0013LV[‘PPa\u0005:V[`\u0000a\u0002˃a\u000e.V[`@Qc&1ò±`á\u001bRf¸\u0017\u0002à\\\u000bo‚\u0011\u0015`\u0004‚\u0001R`\u0000sq\tpžÏ©\u001a€boó˜hö[\u001dÑ-cLcåb`$\u0001`\u0000`@Q€ƒ\u0003`\u0000‡€;\u0015€\u0015a\u0005âW`\u0000€ý[PZñ\u0015€\u0015a\u0005öW=`\u0000€>=`\u0000ý[PPPP`\u0000[‚\u0015a\u0006!Wa\u0006\rƒ‚a\u0013eV[Pa\u0006\u001a`\u0001„a\u0013!V[’Pa\u0005ýV[’‘PPV[`@Qc&1ò±`á\u001bR`d‚\u0011\u0015`\u0004‚\u0001Rsq\tpžÏ©\u001a€boó˜hö[\u001dÑ-cLcåb`$\u0001`\u0000`@Q€ƒ\u0003`\u0000‡€;\u0015€\u0015a\u0006wW`\u0000€ý[PZñ\u0015€\u0015a\u0006‹W=`\u0000€>=`\u0000ý[PPPP`\u0000`\u0002‚`\u0001a\u0006 ‘a\u0013eV[a\u0006ª„a\u0013}V[a\u0006´‘a\u00138V[P`\u0000a\u0004°ƒa\u000eeV[`\u0000a\u0006̂a\u000eV[P`\u0001€[‚Q\u0010€\u0015a\u0006ßWP[\u0015a\u0005\u0012WƒQ\u0010a\u0006öWa\u0006öa\u0013œV[` \u0002` \u0001\u0001Q„`\u0001ƒa\u0007\u000c‘a\u0013!V[Q\u0010a\u0007\u001cWa\u0007\u001ca\u0013œV[` \u0002` \u0001\u0001Q\u0011\u0015‘P€€a\u00073a\u0013LV[‘PPa\u0006ÒV[`\u0000a\u0007Fƒa\u000e»V[P‚`\u0000\u0003a\u0007[Wa\u0003\u0014`\u0000a\u000c’V[a\u0007ga\u0002݂a\tJV[`\u0000a\u0007|a\u0007w`\u0001†a\u0013!V[a\u000e»V[Pa\u0003ƒ„\u0011\u0015€a\u0007WP‚„\u0010\u0015[€a\u0002ÝWPa\u0007Ÿ„a\tJV[\u0015a\t›V[`\u0000€Ta\u0001\u0000\u0004`ÿ\u0016\u0015a\u0007ÅWP`\u0000Ta\u0001\u0000\u0004`ÿ\u0016V[`\u0000sq\tpžÏ©\u001a€boó˜hö[\u001dÑ-;\u0015a\u0008ËW`@€Qsq\tpžÏ©\u001a€boó˜hö[\u001dÑ-` ‚\u0001Re\u0019˜Z[\u0019Y`Ò\u001b‚„\u0001R‚Q€ƒ\u0003„\u0001R``ƒ\u0001“R`\u0000’‘a\u0008S‘fpÊA\u001dpêÕ\r\\\"\u0007\r¯Ãj×_=Ï^r7²*ޚìđ`€\u0001a\u0013ÞV[`@€Q`\u001f\u0019„\u0003\u0001R‚Ra\u0008m‘a\u0014\u000fV[`\u0000`@Q€ƒ\u0003`\u0000†Zñ‘PP=€`\u0000\u0014a\u0008ªW`@Q‘P`\u001f\u0019`?=\u0001\u0016‚\u0001`@R=‚R=`\u0000` „\u0001>a\u0008¯V[``‘P[P‘PP€€` \u0001Q\u0001a\u0008Ǒa\u0014+V[‘PP[‘PV[`\u0000a\u0008ۂa\u000eõV[P`\u0001€[‚Q\u0010€\u0015a\u0008îWP[\u0015a\u0005\u0012WƒQ\u0010a\t\u0005Wa\t\u0005a\u0013œV[` \u0002` \u0001\u0001Q„`\u0001ƒa\t\u001b‘a\u0013!V[Q\u0010a\t+Wa\t+a\u0013œV[` \u0002` \u0001\u0001Q\u0011\u0015‘P€€a\tBa\u0013LV[‘PPa\u0008áV[`\u0000`\u0002‚\u0010\u0015a\t]WP`\u0000‘PV[`\u0002[‚\u0010\u0015a\t’Wa\tr„a\u0012÷V[\u0015a\t€WP`\u0000’‘PPV[€a\tŠa\u0013LV[‘PPa\t`V[P`\u0001’‘PPV[€a\u0003£WA0O¬Ù2=u±\u001bÍÖ\tË8ïÿý°W\u0010÷Êðé±lmpŸP`@Qa\tÿ` €‚R`\u0017‚\u0001RError: Assertion Failed\u0000\u0000\u0000\u0000\u0000\u0000\u0000\u0000\u0000`@‚\u0001R``\u0001V[`@Q€‘\u0003¡a\u0003£a\u000f\u0017V[`\u0000`\u0000\u0003a\n!WP`\u0000‘PV[[€‘P`\u0002a\n3…„a\u0010#V[a\n=‘a\u0013eV[a\nG‘a\u00138V[P\u0003a\n#W[P‘PV[`\u0000g\rඳ§d\u0000\u0000a\nm`\u0002‚a\u00138V[a\nw„†a\u0013}V[a\n‘a\u0013eV[a\n‹‘a\u00138V[“’PPPV[`\u0000`\u0002‚\u0010\u0015a\n¥WP`\u0000‘PV[`\u0002[a\n³`\u0002„a\u00138V[\u0011a\t’Wa\nÁ„a\u0012÷V[\u0015a\nÑWP`\u0000’‘PPV[€a\nہa\u0013LV[‘PPa\n¨V[€\u0015\u0015‚\u0015\u0015\u0014a\u0004\u0006WA0O¬Ù2=u±\u001bÍÖ\tË8ïÿý°W\u0010÷Êðé±lmpŸP`@Qa\u000bX` €‚R`\"‚\u0001RError: a == b not satisfied [boo`@‚\u0001Ral]`ð\u001b``‚\u0001R`€\u0001V[`@Q€‘\u0003¡(\u000fDF²Š\u0013rA}Úe0¹[)’±*ÉÇóxS_)©zÏ5ƒa\u000b©W`@Q€`@\u0001`@R€`\u0005R` \u0001dfalse`Ø\u001bRPa\u000bÇV[`@Q€`@\u0001`@R€`\u0004R` \u0001ctrue`à\u001bRP[`@Qa\u000bԑa\u0014yV[`@Q€‘\u0003¡(\u000fDF²Š\u0013rA}Úe0¹[)’±*ÉÇóxS_)©zÏ5ƒ‚a\u000c%W`@Q€`@\u0001`@R€`\u0005R` \u0001dfalse`Ø\u001bRPa\u000cCV[`@Q€`@\u0001`@R€`\u0004R` \u0001ctrue`à\u001bRP[`@Qa\u000cP‘a\u0014½V[`@Q€‘\u0003¡a\u0004\u0006a\u000f\u0017V[`\u0000€€[ƒ\u0010\u0015a\u000c‹Wa\u000cwƒa\u0013eV[‘P€a\u000cƒa\u0013LV[‘PPa\u000ceV[P’‘PPV[€‚\u0014a\u0004\u0006WA0O¬Ù2=u±\u001bÍÖ\tË8ïÿý°W\u0010÷Êðé±lmpŸP`@Qa\r\u0003` €‚R`\"‚\u0001RError: a == b not satisfied [uin`@‚\u0001Rat]`ð\u001b``‚\u0001R`€\u0001V[`@Q€‘\u0003¡²Þ/¾€\u001a\röÀËÝýD‹£Ä\u001dH @Ê5Ål–ï\u000fÊç!¨`@Qa\r:‘a\u0014çV[`@Q€‘\u0003¡²Þ/¾€\u001a\röÀËÝýD‹£Ä\u001dH @Ê5Ål–ï\u000fÊç!¨‚`@Qa\u000cP‘a\u0015\u001fV[`\u0000€`\u0001[ƒQ\u0010\u0015a\u000c‹W„‚Q\u0010a\r“Wa\r“a\u0013œV[` \u0002` \u0001\u0001Q\u0011\u0015a\r¾WƒQ\u0010a\r³Wa\r³a\u0013œV[` \u0002` \u0001\u0001Q‘P[€a\rȁa\u0013LV[‘PPa\rwV[`\u0000€€[ƒQ\u0010\u0015a\u000c‹W„‚Q\u0010a\rñWa\rña\u0013œV[` \u0002` \u0001\u0001Q\u0011\u0015a\u000e\u001cWƒQ\u0010a\u000e\u0011Wa\u000e\u0011a\u0013œV[` \u0002` \u0001\u0001Q‘P[€a\u000e&a\u0013LV[‘PPa\rÕV[`\u0000`\u0002[‚\u0010\u0015a\t’Wa\u000eE„a\u0012÷V[\u0015a\u000eSWP`\u0000’‘PPV[€a\u000e]a\u0013LV[‘PPa\u000e3V[`\u0000€€[ƒ\u0011a\u000c‹Wa\u000e{ƒa\u0013eV[‘P€a\u000e‡a\u0013LV[‘PPa\u000ejV[```\u0001‚Q\u0011a\u000ežWPV[a\u000e·‚`\u0000`\u0001…Qa\u000e²‘a\u0013!V[a\u0010CV[PV[`\u0000€[‚\u0010\u0015a\nQWa\u000eсa\u0013LV[’PPa\u000e݂a\tJV[\u0015a\u000eðW€a\u000eìa\u0013LV[‘PP[a\u000e¿V[```\u0001‚Q\u0011a\u000f\u0004WPV[a\u000e·‚`\u0001€…Qa\u000e²‘a\u0013!V[sq\tpžÏ©\u001a€boó˜hö[\u001dÑ-;\u0015a\u0010\u0012W`@€Qsq\tpžÏ©\u001a€boó˜hö[\u001dÑ-` ‚\u0001Re\u0019˜Z[\u0019Y`Ò\u001b’‚\u0001’’R`\u0001``‚\u0001R`\u0000‘pÊ\u0010»ÐÛý ©ô±4\u0002Ál± p^\r\u001c\nê±\u000f£S®XoĐ`€\u0001`@€Q`\u001f\u0019„\u0003\u0001R‚Ra\u000f±’‘` \u0001a\u0013ÞV[`@€Q`\u001f\u0019„\u0003\u0001R‚Ra\u000fˑa\u0014\u000fV[`\u0000`@Q€ƒ\u0003`\u0000†Zñ‘PP=€`\u0000\u0014a\u0010\u0008W`@Q‘P`\u001f\u0019`?=\u0001\u0016‚\u0001`@R=‚R=`\u0000` „\u0001>a\u0010\rV[``‘P[PPPP[`\u0000€Taÿ\u0000\u0019\u0016a\u0001\u0000\u0017UV[`\u0000a\u00101`\u0002‚a\u00138V[a\nwg\rඳ§d\u0000\u0000†a\u0013}V[€‚\u0010a\u0010OWPPPV[`\u0000…`\u0002a\u0010`……a\u0013!V[a\u0010j‘a\u00138V[a\u0010t‡a\u0013eV[Q\u0010a\u0010„Wa\u0010„a\u0013œV[` \u0002` \u0001\u0001QP[ƒ\u0011a\u0011¤W[€†„Q\u0010a\u0010ªWa\u0010ªa\u0013œV[` \u0002` \u0001\u0001Q\u0010\u0015a\u0010ÊW‚a\u0010a\u0013LV[“PPa\u0010—V[…‚Q\u0010a\u0010ÜWa\u0010Üa\u0013œV[` \u0002` \u0001\u0001Q\u0010€\u0015a\u0010òWP`\u0000‚\u0011[\u0015a\u0011\tWa\u0011\u0001a\u0015IV[’PPa\u0010ÊV[ƒ\u0011a\u0011ŸW…‚Q\u0010a\u0011\"Wa\u0011\"a\u0013œV[` \u0002` \u0001\u0001Q†„Q\u0010a\u0011=`\u0000ý[PPPP`\u0000`\u0002‚`\u0001a\u0004‘a\u0013eV[a\u0004™„a\u0013}V[a\u0004£‘a\u00138V[P`\u0000a\u0004°ƒa\u000c`V[Pa\u0003\u0014‚‚a\u000c’V[`\u0000a\u0004ǂa\rqV[P`\u0001`\u0000[ƒQ\u0010€\u0015a\u0004ÛWP[\u0015a\u0005\u0012WƒQ\u0010a\u0004òWa\u0004òa\u0013œV[` \u0002` \u0001\u0001Qƒ\u0010\u0015‘P€€a\u0005\na\u0013LV[‘PPa\u0004ÎV[Pa\u0003\u0014a\t›V[`\u0000a\u0003&`da\u0005‰V[`\u0000a\u00053‚a\rÐV[P`\u0001`\u0000[ƒQ\u0010€\u0015a\u0005GWP[\u0015a\u0005\u0012WƒQ\u0010a\u0005^Wa\u0005^a\u0013œV[` \u0002` \u0001\u0001Qƒ\u0010\u0015‘P€€a\u0005va\u0013LV[‘PPa\u0005:V[`\u0000a\u0002˃a\u000e.V[`@Qc&1ò±`á\u001bRf¸\u0017\u0002à\\\u000bo‚\u0011\u0015`\u0004‚\u0001R`\u0000sq\tpžÏ©\u001a€boó˜hö[\u001dÑ-cLcåb`$\u0001`\u0000`@Q€ƒ\u0003`\u0000‡€;\u0015€\u0015a\u0005âW`\u0000€ý[PZñ\u0015€\u0015a\u0005öW=`\u0000€>=`\u0000ý[PPPP`\u0000[‚\u0015a\u0006!Wa\u0006\rƒ‚a\u0013eV[Pa\u0006\u001a`\u0001„a\u0013!V[’Pa\u0005ýV[’‘PPV[`@Qc&1ò±`á\u001bR`d‚\u0011\u0015`\u0004‚\u0001Rsq\tpžÏ©\u001a€boó˜hö[\u001dÑ-cLcåb`$\u0001`\u0000`@Q€ƒ\u0003`\u0000‡€;\u0015€\u0015a\u0006wW`\u0000€ý[PZñ\u0015€\u0015a\u0006‹W=`\u0000€>=`\u0000ý[PPPP`\u0000`\u0002‚`\u0001a\u0006 ‘a\u0013eV[a\u0006ª„a\u0013}V[a\u0006´‘a\u00138V[P`\u0000a\u0004°ƒa\u000eeV[`\u0000a\u0006̂a\u000eV[P`\u0001€[‚Q\u0010€\u0015a\u0006ßWP[\u0015a\u0005\u0012WƒQ\u0010a\u0006öWa\u0006öa\u0013œV[` \u0002` \u0001\u0001Q„`\u0001ƒa\u0007\u000c‘a\u0013!V[Q\u0010a\u0007\u001cWa\u0007\u001ca\u0013œV[` \u0002` \u0001\u0001Q\u0011\u0015‘P€€a\u00073a\u0013LV[‘PPa\u0006ÒV[`\u0000a\u0007Fƒa\u000e»V[P‚`\u0000\u0003a\u0007[Wa\u0003\u0014`\u0000a\u000c’V[a\u0007ga\u0002݂a\tJV[`\u0000a\u0007|a\u0007w`\u0001†a\u0013!V[a\u000e»V[Pa\u0003ƒ„\u0011\u0015€a\u0007WP‚„\u0010\u0015[€a\u0002ÝWPa\u0007Ÿ„a\tJV[\u0015a\t›V[`\u0000€Ta\u0001\u0000\u0004`ÿ\u0016\u0015a\u0007ÅWP`\u0000Ta\u0001\u0000\u0004`ÿ\u0016V[`\u0000sq\tpžÏ©\u001a€boó˜hö[\u001dÑ-;\u0015a\u0008ËW`@€Qsq\tpžÏ©\u001a€boó˜hö[\u001dÑ-` ‚\u0001Re\u0019˜Z[\u0019Y`Ò\u001b‚„\u0001R‚Q€ƒ\u0003„\u0001R``ƒ\u0001“R`\u0000’‘a\u0008S‘fpÊA\u001dpêÕ\r\\\"\u0007\r¯Ãj×_=Ï^r7²*ޚìđ`€\u0001a\u0013ÞV[`@€Q`\u001f\u0019„\u0003\u0001R‚Ra\u0008m‘a\u0014\u000fV[`\u0000`@Q€ƒ\u0003`\u0000†Zñ‘PP=€`\u0000\u0014a\u0008ªW`@Q‘P`\u001f\u0019`?=\u0001\u0016‚\u0001`@R=‚R=`\u0000` „\u0001>a\u0008¯V[``‘P[P‘PP€€` \u0001Q\u0001a\u0008Ǒa\u0014+V[‘PP[‘PV[`\u0000a\u0008ۂa\u000eõV[P`\u0001€[‚Q\u0010€\u0015a\u0008îWP[\u0015a\u0005\u0012WƒQ\u0010a\t\u0005Wa\t\u0005a\u0013œV[` \u0002` \u0001\u0001Q„`\u0001ƒa\t\u001b‘a\u0013!V[Q\u0010a\t+Wa\t+a\u0013œV[` \u0002` \u0001\u0001Q\u0011\u0015‘P€€a\tBa\u0013LV[‘PPa\u0008áV[`\u0000`\u0002‚\u0010\u0015a\t]WP`\u0000‘PV[`\u0002[‚\u0010\u0015a\t’Wa\tr„a\u0012÷V[\u0015a\t€WP`\u0000’‘PPV[€a\tŠa\u0013LV[‘PPa\t`V[P`\u0001’‘PPV[€a\u0003£WA0O¬Ù2=u±\u001bÍÖ\tË8ïÿý°W\u0010÷Êðé±lmpŸP`@Qa\tÿ` €‚R`\u0017‚\u0001RError: Assertion Failed\u0000\u0000\u0000\u0000\u0000\u0000\u0000\u0000\u0000`@‚\u0001R``\u0001V[`@Q€‘\u0003¡a\u0003£a\u000f\u0017V[`\u0000`\u0000\u0003a\n!WP`\u0000‘PV[[€‘P`\u0002a\n3…„a\u0010#V[a\n=‘a\u0013eV[a\nG‘a\u00138V[P\u0003a\n#W[P‘PV[`\u0000g\rඳ§d\u0000\u0000a\nm`\u0002‚a\u00138V[a\nw„†a\u0013}V[a\n‘a\u0013eV[a\n‹‘a\u00138V[“’PPPV[`\u0000`\u0002‚\u0010\u0015a\n¥WP`\u0000‘PV[`\u0002[a\n³`\u0002„a\u00138V[\u0011a\t’Wa\nÁ„a\u0012÷V[\u0015a\nÑWP`\u0000’‘PPV[€a\nہa\u0013LV[‘PPa\n¨V[€\u0015\u0015‚\u0015\u0015\u0014a\u0004\u0006WA0O¬Ù2=u±\u001bÍÖ\tË8ïÿý°W\u0010÷Êðé±lmpŸP`@Qa\u000bX` €‚R`\"‚\u0001RError: a == b not satisfied [boo`@‚\u0001Ral]`ð\u001b``‚\u0001R`€\u0001V[`@Q€‘\u0003¡(\u000fDF²Š\u0013rA}Úe0¹[)’±*ÉÇóxS_)©zÏ5ƒa\u000b©W`@Q€`@\u0001`@R€`\u0005R` \u0001dfalse`Ø\u001bRPa\u000bÇV[`@Q€`@\u0001`@R€`\u0004R` \u0001ctrue`à\u001bRP[`@Qa\u000bԑa\u0014yV[`@Q€‘\u0003¡(\u000fDF²Š\u0013rA}Úe0¹[)’±*ÉÇóxS_)©zÏ5ƒ‚a\u000c%W`@Q€`@\u0001`@R€`\u0005R` \u0001dfalse`Ø\u001bRPa\u000cCV[`@Q€`@\u0001`@R€`\u0004R` \u0001ctrue`à\u001bRP[`@Qa\u000cP‘a\u0014½V[`@Q€‘\u0003¡a\u0004\u0006a\u000f\u0017V[`\u0000€€[ƒ\u0010\u0015a\u000c‹Wa\u000cwƒa\u0013eV[‘P€a\u000cƒa\u0013LV[‘PPa\u000ceV[P’‘PPV[€‚\u0014a\u0004\u0006WA0O¬Ù2=u±\u001bÍÖ\tË8ïÿý°W\u0010÷Êðé±lmpŸP`@Qa\r\u0003` €‚R`\"‚\u0001RError: a == b not satisfied [uin`@‚\u0001Rat]`ð\u001b``‚\u0001R`€\u0001V[`@Q€‘\u0003¡²Þ/¾€\u001a\röÀËÝýD‹£Ä\u001dH @Ê5Ål–ï\u000fÊç!¨`@Qa\r:‘a\u0014çV[`@Q€‘\u0003¡²Þ/¾€\u001a\röÀËÝýD‹£Ä\u001dH @Ê5Ål–ï\u000fÊç!¨‚`@Qa\u000cP‘a\u0015\u001fV[`\u0000€`\u0001[ƒQ\u0010\u0015a\u000c‹W„‚Q\u0010a\r“Wa\r“a\u0013œV[` \u0002` \u0001\u0001Q\u0011\u0015a\r¾WƒQ\u0010a\r³Wa\r³a\u0013œV[` \u0002` \u0001\u0001Q‘P[€a\rȁa\u0013LV[‘PPa\rwV[`\u0000€€[ƒQ\u0010\u0015a\u000c‹W„‚Q\u0010a\rñWa\rña\u0013œV[` \u0002` \u0001\u0001Q\u0011\u0015a\u000e\u001cWƒQ\u0010a\u000e\u0011Wa\u000e\u0011a\u0013œV[` \u0002` \u0001\u0001Q‘P[€a\u000e&a\u0013LV[‘PPa\rÕV[`\u0000`\u0002[‚\u0010\u0015a\t’Wa\u000eE„a\u0012÷V[\u0015a\u000eSWP`\u0000’‘PPV[€a\u000e]a\u0013LV[‘PPa\u000e3V[`\u0000€€[ƒ\u0011a\u000c‹Wa\u000e{ƒa\u0013eV[‘P€a\u000e‡a\u0013LV[‘PPa\u000ejV[```\u0001‚Q\u0011a\u000ežWPV[a\u000e·‚`\u0000`\u0001…Qa\u000e²‘a\u0013!V[a\u0010CV[PV[`\u0000€[‚\u0010\u0015a\nQWa\u000eсa\u0013LV[’PPa\u000e݂a\tJV[\u0015a\u000eðW€a\u000eìa\u0013LV[‘PP[a\u000e¿V[```\u0001‚Q\u0011a\u000f\u0004WPV[a\u000e·‚`\u0001€…Qa\u000e²‘a\u0013!V[sq\tpžÏ©\u001a€boó˜hö[\u001dÑ-;\u0015a\u0010\u0012W`@€Qsq\tpžÏ©\u001a€boó˜hö[\u001dÑ-` ‚\u0001Re\u0019˜Z[\u0019Y`Ò\u001b’‚\u0001’’R`\u0001``‚\u0001R`\u0000‘pÊ\u0010»ÐÛý ©ô±4\u0002Ál± p^\r\u001c\nê±\u000f£S®XoĐ`€\u0001`@€Q`\u001f\u0019„\u0003\u0001R‚Ra\u000f±’‘` \u0001a\u0013ÞV[`@€Q`\u001f\u0019„\u0003\u0001R‚Ra\u000fˑa\u0014\u000fV[`\u0000`@Q€ƒ\u0003`\u0000†Zñ‘PP=€`\u0000\u0014a\u0010\u0008W`@Q‘P`\u001f\u0019`?=\u0001\u0016‚\u0001`@R=‚R=`\u0000` „\u0001>a\u0010\rV[``‘P[PPPP[`\u0000€Taÿ\u0000\u0019\u0016a\u0001\u0000\u0017UV[`\u0000a\u00101`\u0002‚a\u00138V[a\nwg\rඳ§d\u0000\u0000†a\u0013}V[€‚\u0010a\u0010OWPPPV[`\u0000…`\u0002a\u0010`……a\u0013!V[a\u0010j‘a\u00138V[a\u0010t‡a\u0013eV[Q\u0010a\u0010„Wa\u0010„a\u0013œV[` \u0002` \u0001\u0001QP[ƒ\u0011a\u0011¤W[€†„Q\u0010a\u0010ªWa\u0010ªa\u0013œV[` \u0002` \u0001\u0001Q\u0010\u0015a\u0010ÊW‚a\u0010a\u0013LV[“PPa\u0010—V[…‚Q\u0010a\u0010ÜWa\u0010Üa\u0013œV[` \u0002` \u0001\u0001Q\u0010€\u0015a\u0010òWP`\u0000‚\u0011[\u0015a\u0011\tWa\u0011\u0001a\u0015IV[’PPa\u0010ÊV[ƒ\u0011a\u0011ŸW…‚Q\u0010a\u0011\"Wa\u0011\"a\u0013œV[` \u0002` \u0001\u0001Q†„Q\u0010a\u0011` configuration — so the matcher returns `MatchSuccess` — but differ in their attached path-condition predicates. +The leftover consequent predicate is then simplified under the antecedent and any residue is SMT-closed, so the verdict turns on linear-integer reasoning rather than syntactic matching. +The definition (`resources/implies-smt.k`) is just `configuration $PGM:Int ` over `INT`/`BOOL`. + +The cases cover each arm of the discharge logic, and `002` deliberately diverges between the two engines: booster's SMT cannot refute the obligation and returns `indeterminate` (the signal for a recover-mode client to escalate), whereas kore decides it. +`005` is the same query as `002` but with `assume-defined: true`, which makes the proxy run booster first and then escalate the `indeterminate` verdict to kore — so the booster-dev server reports `indeterminate` while the full proxy reports kore's `invalid`. + +| test | antecedent ⟹ consequent | booster-dev `status` | proxy/kore `status` | arm exercised | +|---------------------------|--------------------------------------|----------------------|---------------------|--------------------------------------------------| +| 001-bound-weakening | `X .json` (kore / default server) and `response-.booster-dev` (booster-dev server). diff --git a/booster/test/rpc-integration/test-implies-smt/response-001-bound-weakening.booster-dev b/booster/test/rpc-integration/test-implies-smt/response-001-bound-weakening.booster-dev new file mode 100644 index 0000000000..9b74735a67 --- /dev/null +++ b/booster/test/rpc-integration/test-implies-smt/response-001-bound-weakening.booster-dev @@ -0,0 +1,63 @@ +{ + "jsonrpc": "2.0", + "id": "implies-smt-001", + "result": { + "status": "valid", + "implication": { + "format": "KORE", + "version": 1, + "term": { + "tag": "Implies", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + }, + "first": { + "tag": "EVar", + "name": "VarX", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + } + }, + "second": { + "tag": "EVar", + "name": "VarX", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + } + } + } + }, + "condition": { + "substitution": { + "format": "KORE", + "version": 1, + "term": { + "tag": "Top", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + } + } + }, + "predicate": { + "format": "KORE", + "version": 1, + "term": { + "tag": "Top", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + } + } + } + } + } +} \ No newline at end of file diff --git a/booster/test/rpc-integration/test-implies-smt/response-001-bound-weakening.json b/booster/test/rpc-integration/test-implies-smt/response-001-bound-weakening.json new file mode 100644 index 0000000000..00fb7eb704 --- /dev/null +++ b/booster/test/rpc-integration/test-implies-smt/response-001-bound-weakening.json @@ -0,0 +1,177 @@ +{ + "jsonrpc": "2.0", + "id": "implies-smt-001", + "result": { + "status": "valid", + "implication": { + "format": "KORE", + "version": 1, + "term": { + "tag": "Implies", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + }, + "first": { + "tag": "And", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + }, + "patterns": [ + { + "tag": "EVar", + "name": "VarX", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + } + }, + { + "tag": "Equals", + "argSort": { + "tag": "SortApp", + "name": "SortBool", + "args": [] + }, + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + }, + "first": { + "tag": "DV", + "sort": { + "tag": "SortApp", + "name": "SortBool", + "args": [] + }, + "value": "true" + }, + "second": { + "tag": "App", + "name": "Lbl'Unds-LT-'Int'Unds'", + "sorts": [], + "args": [ + { + "tag": "EVar", + "name": "VarX", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + } + }, + { + "tag": "DV", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + }, + "value": "100" + } + ] + } + } + ] + }, + "second": { + "tag": "And", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + }, + "patterns": [ + { + "tag": "EVar", + "name": "VarX", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + } + }, + { + "tag": "Equals", + "argSort": { + "tag": "SortApp", + "name": "SortBool", + "args": [] + }, + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + }, + "first": { + "tag": "DV", + "sort": { + "tag": "SortApp", + "name": "SortBool", + "args": [] + }, + "value": "true" + }, + "second": { + "tag": "App", + "name": "Lbl'Unds-LT-'Int'Unds'", + "sorts": [], + "args": [ + { + "tag": "EVar", + "name": "VarX", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + } + }, + { + "tag": "DV", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + }, + "value": "1000" + } + ] + } + } + ] + } + } + }, + "condition": { + "substitution": { + "format": "KORE", + "version": 1, + "term": { + "tag": "Top", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + } + } + }, + "predicate": { + "format": "KORE", + "version": 1, + "term": { + "tag": "Top", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + } + } + } + } + } +} \ No newline at end of file diff --git a/booster/test/rpc-integration/test-implies-smt/response-002-does-not-imply.booster-dev b/booster/test/rpc-integration/test-implies-smt/response-002-does-not-imply.booster-dev new file mode 100644 index 0000000000..2a7c3870d4 --- /dev/null +++ b/booster/test/rpc-integration/test-implies-smt/response-002-does-not-imply.booster-dev @@ -0,0 +1,37 @@ +{ + "jsonrpc": "2.0", + "id": "implies-smt-002", + "result": { + "status": "indeterminate", + "implication": { + "format": "KORE", + "version": 1, + "term": { + "tag": "Implies", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + }, + "first": { + "tag": "EVar", + "name": "VarX", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + } + }, + "second": { + "tag": "EVar", + "name": "VarX", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + } + } + } + } + } +} \ No newline at end of file diff --git a/booster/test/rpc-integration/test-implies-smt/response-002-does-not-imply.json b/booster/test/rpc-integration/test-implies-smt/response-002-does-not-imply.json new file mode 100644 index 0000000000..d02048bcec --- /dev/null +++ b/booster/test/rpc-integration/test-implies-smt/response-002-does-not-imply.json @@ -0,0 +1,177 @@ +{ + "jsonrpc": "2.0", + "id": "implies-smt-002", + "result": { + "status": "invalid", + "implication": { + "format": "KORE", + "version": 1, + "term": { + "tag": "Implies", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + }, + "first": { + "tag": "And", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + }, + "patterns": [ + { + "tag": "EVar", + "name": "VarX", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + } + }, + { + "tag": "Equals", + "argSort": { + "tag": "SortApp", + "name": "SortBool", + "args": [] + }, + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + }, + "first": { + "tag": "DV", + "sort": { + "tag": "SortApp", + "name": "SortBool", + "args": [] + }, + "value": "true" + }, + "second": { + "tag": "App", + "name": "Lbl'Unds-LT-'Int'Unds'", + "sorts": [], + "args": [ + { + "tag": "EVar", + "name": "VarX", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + } + }, + { + "tag": "DV", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + }, + "value": "100" + } + ] + } + } + ] + }, + "second": { + "tag": "And", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + }, + "patterns": [ + { + "tag": "EVar", + "name": "VarX", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + } + }, + { + "tag": "Equals", + "argSort": { + "tag": "SortApp", + "name": "SortBool", + "args": [] + }, + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + }, + "first": { + "tag": "DV", + "sort": { + "tag": "SortApp", + "name": "SortBool", + "args": [] + }, + "value": "true" + }, + "second": { + "tag": "App", + "name": "Lbl'Unds-LT-'Int'Unds'", + "sorts": [], + "args": [ + { + "tag": "EVar", + "name": "VarX", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + } + }, + { + "tag": "DV", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + }, + "value": "10" + } + ] + } + } + ] + } + } + }, + "condition": { + "substitution": { + "format": "KORE", + "version": 1, + "term": { + "tag": "Top", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + } + } + }, + "predicate": { + "format": "KORE", + "version": 1, + "term": { + "tag": "Top", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + } + } + } + } + } +} \ No newline at end of file diff --git a/booster/test/rpc-integration/test-implies-smt/response-003-vacuous-antecedent.booster-dev b/booster/test/rpc-integration/test-implies-smt/response-003-vacuous-antecedent.booster-dev new file mode 100644 index 0000000000..ebbb867dcf --- /dev/null +++ b/booster/test/rpc-integration/test-implies-smt/response-003-vacuous-antecedent.booster-dev @@ -0,0 +1,209 @@ +{ + "jsonrpc": "2.0", + "id": "implies-smt-003", + "result": { + "status": "valid", + "implication": { + "format": "KORE", + "version": 1, + "term": { + "tag": "Implies", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + }, + "first": { + "tag": "And", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + }, + "patterns": [ + { + "tag": "EVar", + "name": "VarX", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + } + }, + { + "tag": "Equals", + "argSort": { + "tag": "SortApp", + "name": "SortBool", + "args": [] + }, + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + }, + "first": { + "tag": "DV", + "sort": { + "tag": "SortApp", + "name": "SortBool", + "args": [] + }, + "value": "true" + }, + "second": { + "tag": "App", + "name": "Lbl'Unds'andBool'Unds'", + "sorts": [], + "args": [ + { + "tag": "App", + "name": "Lbl'Unds-LT-'Int'Unds'", + "sorts": [], + "args": [ + { + "tag": "EVar", + "name": "VarX", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + } + }, + { + "tag": "DV", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + }, + "value": "10" + } + ] + }, + { + "tag": "App", + "name": "Lbl'Unds-LT-'Int'Unds'", + "sorts": [], + "args": [ + { + "tag": "DV", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + }, + "value": "20" + }, + { + "tag": "EVar", + "name": "VarX", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + } + } + ] + } + ] + } + } + ] + }, + "second": { + "tag": "And", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + }, + "patterns": [ + { + "tag": "EVar", + "name": "VarX", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + } + }, + { + "tag": "Equals", + "argSort": { + "tag": "SortApp", + "name": "SortBool", + "args": [] + }, + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + }, + "first": { + "tag": "DV", + "sort": { + "tag": "SortApp", + "name": "SortBool", + "args": [] + }, + "value": "true" + }, + "second": { + "tag": "App", + "name": "Lbl'Unds-LT-'Int'Unds'", + "sorts": [], + "args": [ + { + "tag": "EVar", + "name": "VarX", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + } + }, + { + "tag": "DV", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + }, + "value": "1000" + } + ] + } + } + ] + } + } + }, + "condition": { + "substitution": { + "format": "KORE", + "version": 1, + "term": { + "tag": "Top", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + } + } + }, + "predicate": { + "format": "KORE", + "version": 1, + "term": { + "tag": "Bottom", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + } + } + } + } + } +} \ No newline at end of file diff --git a/booster/test/rpc-integration/test-implies-smt/response-003-vacuous-antecedent.json b/booster/test/rpc-integration/test-implies-smt/response-003-vacuous-antecedent.json new file mode 100644 index 0000000000..f9fe646c2a --- /dev/null +++ b/booster/test/rpc-integration/test-implies-smt/response-003-vacuous-antecedent.json @@ -0,0 +1,234 @@ +{ + "jsonrpc": "2.0", + "id": "implies-smt-003", + "result": { + "status": "valid", + "implication": { + "format": "KORE", + "version": 1, + "term": { + "tag": "Implies", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + }, + "first": { + "tag": "And", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + }, + "patterns": [ + { + "tag": "EVar", + "name": "VarX", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + } + }, + { + "tag": "And", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + }, + "patterns": [ + { + "tag": "Equals", + "argSort": { + "tag": "SortApp", + "name": "SortBool", + "args": [] + }, + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + }, + "first": { + "tag": "DV", + "sort": { + "tag": "SortApp", + "name": "SortBool", + "args": [] + }, + "value": "true" + }, + "second": { + "tag": "App", + "name": "Lbl'Unds-LT-'Int'Unds'", + "sorts": [], + "args": [ + { + "tag": "DV", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + }, + "value": "20" + }, + { + "tag": "EVar", + "name": "VarX", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + } + } + ] + } + }, + { + "tag": "Equals", + "argSort": { + "tag": "SortApp", + "name": "SortBool", + "args": [] + }, + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + }, + "first": { + "tag": "DV", + "sort": { + "tag": "SortApp", + "name": "SortBool", + "args": [] + }, + "value": "true" + }, + "second": { + "tag": "App", + "name": "Lbl'Unds-LT-'Int'Unds'", + "sorts": [], + "args": [ + { + "tag": "EVar", + "name": "VarX", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + } + }, + { + "tag": "DV", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + }, + "value": "10" + } + ] + } + } + ] + } + ] + }, + "second": { + "tag": "And", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + }, + "patterns": [ + { + "tag": "EVar", + "name": "VarX", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + } + }, + { + "tag": "Equals", + "argSort": { + "tag": "SortApp", + "name": "SortBool", + "args": [] + }, + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + }, + "first": { + "tag": "DV", + "sort": { + "tag": "SortApp", + "name": "SortBool", + "args": [] + }, + "value": "true" + }, + "second": { + "tag": "App", + "name": "Lbl'Unds-LT-'Int'Unds'", + "sorts": [], + "args": [ + { + "tag": "EVar", + "name": "VarX", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + } + }, + { + "tag": "DV", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + }, + "value": "1000" + } + ] + } + } + ] + } + } + }, + "condition": { + "substitution": { + "format": "KORE", + "version": 1, + "term": { + "tag": "Top", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + } + } + }, + "predicate": { + "format": "KORE", + "version": 1, + "term": { + "tag": "Bottom", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + } + } + } + } + } +} \ No newline at end of file diff --git a/booster/test/rpc-integration/test-implies-smt/response-004-address-bound.booster-dev b/booster/test/rpc-integration/test-implies-smt/response-004-address-bound.booster-dev new file mode 100644 index 0000000000..6bd709237a --- /dev/null +++ b/booster/test/rpc-integration/test-implies-smt/response-004-address-bound.booster-dev @@ -0,0 +1,63 @@ +{ + "jsonrpc": "2.0", + "id": "implies-smt-004", + "result": { + "status": "valid", + "implication": { + "format": "KORE", + "version": 1, + "term": { + "tag": "Implies", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + }, + "first": { + "tag": "EVar", + "name": "VarACCT'Unds'ID", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + } + }, + "second": { + "tag": "EVar", + "name": "VarACCT'Unds'ID", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + } + } + } + }, + "condition": { + "substitution": { + "format": "KORE", + "version": 1, + "term": { + "tag": "Top", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + } + } + }, + "predicate": { + "format": "KORE", + "version": 1, + "term": { + "tag": "Top", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + } + } + } + } + } +} \ No newline at end of file diff --git a/booster/test/rpc-integration/test-implies-smt/response-004-address-bound.json b/booster/test/rpc-integration/test-implies-smt/response-004-address-bound.json new file mode 100644 index 0000000000..a7ec931002 --- /dev/null +++ b/booster/test/rpc-integration/test-implies-smt/response-004-address-bound.json @@ -0,0 +1,234 @@ +{ + "jsonrpc": "2.0", + "id": "implies-smt-004", + "result": { + "status": "valid", + "implication": { + "format": "KORE", + "version": 1, + "term": { + "tag": "Implies", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + }, + "first": { + "tag": "And", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + }, + "patterns": [ + { + "tag": "EVar", + "name": "VarACCT'Unds'ID", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + } + }, + { + "tag": "And", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + }, + "patterns": [ + { + "tag": "Equals", + "argSort": { + "tag": "SortApp", + "name": "SortBool", + "args": [] + }, + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + }, + "first": { + "tag": "DV", + "sort": { + "tag": "SortApp", + "name": "SortBool", + "args": [] + }, + "value": "true" + }, + "second": { + "tag": "App", + "name": "Lbl'Unds-LT-'Int'Unds'", + "sorts": [], + "args": [ + { + "tag": "EVar", + "name": "VarACCT'Unds'ID", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + } + }, + { + "tag": "DV", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + }, + "value": "1461501637330902918203684832716283019655932542976" + } + ] + } + }, + { + "tag": "Equals", + "argSort": { + "tag": "SortApp", + "name": "SortBool", + "args": [] + }, + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + }, + "first": { + "tag": "DV", + "sort": { + "tag": "SortApp", + "name": "SortBool", + "args": [] + }, + "value": "true" + }, + "second": { + "tag": "App", + "name": "Lbl'Unds-LT-Eqls'Int'Unds'", + "sorts": [], + "args": [ + { + "tag": "DV", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + }, + "value": "0" + }, + { + "tag": "EVar", + "name": "VarACCT'Unds'ID", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + } + } + ] + } + } + ] + } + ] + }, + "second": { + "tag": "And", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + }, + "patterns": [ + { + "tag": "EVar", + "name": "VarACCT'Unds'ID", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + } + }, + { + "tag": "Equals", + "argSort": { + "tag": "SortApp", + "name": "SortBool", + "args": [] + }, + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + }, + "first": { + "tag": "DV", + "sort": { + "tag": "SortApp", + "name": "SortBool", + "args": [] + }, + "value": "true" + }, + "second": { + "tag": "App", + "name": "Lbl'Unds-LT-'Int'Unds'", + "sorts": [], + "args": [ + { + "tag": "EVar", + "name": "VarACCT'Unds'ID", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + } + }, + { + "tag": "DV", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + }, + "value": "115792089237316195423570985008687907853269984665640564039457584007913129639936" + } + ] + } + } + ] + } + } + }, + "condition": { + "substitution": { + "format": "KORE", + "version": 1, + "term": { + "tag": "Top", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + } + } + }, + "predicate": { + "format": "KORE", + "version": 1, + "term": { + "tag": "Top", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + } + } + } + } + } +} \ No newline at end of file diff --git a/booster/test/rpc-integration/test-implies-smt/response-005-escalate-indeterminate.booster-dev b/booster/test/rpc-integration/test-implies-smt/response-005-escalate-indeterminate.booster-dev new file mode 100644 index 0000000000..925fe6f1b9 --- /dev/null +++ b/booster/test/rpc-integration/test-implies-smt/response-005-escalate-indeterminate.booster-dev @@ -0,0 +1,37 @@ +{ + "jsonrpc": "2.0", + "id": "implies-smt-005", + "result": { + "status": "indeterminate", + "implication": { + "format": "KORE", + "version": 1, + "term": { + "tag": "Implies", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + }, + "first": { + "tag": "EVar", + "name": "VarX", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + } + }, + "second": { + "tag": "EVar", + "name": "VarX", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + } + } + } + } + } +} \ No newline at end of file diff --git a/booster/test/rpc-integration/test-implies-smt/response-005-escalate-indeterminate.json b/booster/test/rpc-integration/test-implies-smt/response-005-escalate-indeterminate.json new file mode 100644 index 0000000000..c6f4808edc --- /dev/null +++ b/booster/test/rpc-integration/test-implies-smt/response-005-escalate-indeterminate.json @@ -0,0 +1,177 @@ +{ + "jsonrpc": "2.0", + "id": "implies-smt-005", + "result": { + "status": "invalid", + "implication": { + "format": "KORE", + "version": 1, + "term": { + "tag": "Implies", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + }, + "first": { + "tag": "And", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + }, + "patterns": [ + { + "tag": "EVar", + "name": "VarX", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + } + }, + { + "tag": "Equals", + "argSort": { + "tag": "SortApp", + "name": "SortBool", + "args": [] + }, + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + }, + "first": { + "tag": "DV", + "sort": { + "tag": "SortApp", + "name": "SortBool", + "args": [] + }, + "value": "true" + }, + "second": { + "tag": "App", + "name": "Lbl'Unds-LT-'Int'Unds'", + "sorts": [], + "args": [ + { + "tag": "EVar", + "name": "VarX", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + } + }, + { + "tag": "DV", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + }, + "value": "100" + } + ] + } + } + ] + }, + "second": { + "tag": "And", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + }, + "patterns": [ + { + "tag": "EVar", + "name": "VarX", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + } + }, + { + "tag": "Equals", + "argSort": { + "tag": "SortApp", + "name": "SortBool", + "args": [] + }, + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + }, + "first": { + "tag": "DV", + "sort": { + "tag": "SortApp", + "name": "SortBool", + "args": [] + }, + "value": "true" + }, + "second": { + "tag": "App", + "name": "Lbl'Unds-LT-'Int'Unds'", + "sorts": [], + "args": [ + { + "tag": "EVar", + "name": "VarX", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + } + }, + { + "tag": "DV", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + }, + "value": "10" + } + ] + } + } + ] + } + } + }, + "condition": { + "substitution": { + "format": "KORE", + "version": 1, + "term": { + "tag": "Top", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + } + } + }, + "predicate": { + "format": "KORE", + "version": 1, + "term": { + "tag": "Top", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + } + } + } + } + } +} \ No newline at end of file diff --git a/booster/test/rpc-integration/test-implies-smt/state-001-bound-weakening.send b/booster/test/rpc-integration/test-implies-smt/state-001-bound-weakening.send new file mode 100644 index 0000000000..4360db1b9b --- /dev/null +++ b/booster/test/rpc-integration/test-implies-smt/state-001-bound-weakening.send @@ -0,0 +1,59 @@ +{ + "jsonrpc": "2.0", + "id": "implies-smt-001", + "method": "implies", + "params": { + "antecedent": { + "format": "KORE", + "version": 1, + "term": { + "tag": "And", + "sort": {"tag": "SortApp", "name": "SortInt", "args": []}, + "patterns": [ + {"tag": "EVar", "name": "VarX", "sort": {"tag": "SortApp", "name": "SortInt", "args": []}}, + { + "tag": "Equals", + "argSort": {"tag": "SortApp", "name": "SortBool", "args": []}, + "sort": {"tag": "SortApp", "name": "SortInt", "args": []}, + "first": {"tag": "DV", "sort": {"tag": "SortApp", "name": "SortBool", "args": []}, "value": "true"}, + "second": { + "tag": "App", + "name": "Lbl'Unds-LT-'Int'Unds'", + "sorts": [], + "args": [ + {"tag": "EVar", "name": "VarX", "sort": {"tag": "SortApp", "name": "SortInt", "args": []}}, + {"tag": "DV", "sort": {"tag": "SortApp", "name": "SortInt", "args": []}, "value": "100"} + ] + } + } + ] + } + }, + "consequent": { + "format": "KORE", + "version": 1, + "term": { + "tag": "And", + "sort": {"tag": "SortApp", "name": "SortInt", "args": []}, + "patterns": [ + {"tag": "EVar", "name": "VarX", "sort": {"tag": "SortApp", "name": "SortInt", "args": []}}, + { + "tag": "Equals", + "argSort": {"tag": "SortApp", "name": "SortBool", "args": []}, + "sort": {"tag": "SortApp", "name": "SortInt", "args": []}, + "first": {"tag": "DV", "sort": {"tag": "SortApp", "name": "SortBool", "args": []}, "value": "true"}, + "second": { + "tag": "App", + "name": "Lbl'Unds-LT-'Int'Unds'", + "sorts": [], + "args": [ + {"tag": "EVar", "name": "VarX", "sort": {"tag": "SortApp", "name": "SortInt", "args": []}}, + {"tag": "DV", "sort": {"tag": "SortApp", "name": "SortInt", "args": []}, "value": "1000"} + ] + } + } + ] + } + } + } +} diff --git a/booster/test/rpc-integration/test-implies-smt/state-002-does-not-imply.send b/booster/test/rpc-integration/test-implies-smt/state-002-does-not-imply.send new file mode 100644 index 0000000000..9ef5d633b2 --- /dev/null +++ b/booster/test/rpc-integration/test-implies-smt/state-002-does-not-imply.send @@ -0,0 +1,59 @@ +{ + "jsonrpc": "2.0", + "id": "implies-smt-002", + "method": "implies", + "params": { + "antecedent": { + "format": "KORE", + "version": 1, + "term": { + "tag": "And", + "sort": {"tag": "SortApp", "name": "SortInt", "args": []}, + "patterns": [ + {"tag": "EVar", "name": "VarX", "sort": {"tag": "SortApp", "name": "SortInt", "args": []}}, + { + "tag": "Equals", + "argSort": {"tag": "SortApp", "name": "SortBool", "args": []}, + "sort": {"tag": "SortApp", "name": "SortInt", "args": []}, + "first": {"tag": "DV", "sort": {"tag": "SortApp", "name": "SortBool", "args": []}, "value": "true"}, + "second": { + "tag": "App", + "name": "Lbl'Unds-LT-'Int'Unds'", + "sorts": [], + "args": [ + {"tag": "EVar", "name": "VarX", "sort": {"tag": "SortApp", "name": "SortInt", "args": []}}, + {"tag": "DV", "sort": {"tag": "SortApp", "name": "SortInt", "args": []}, "value": "100"} + ] + } + } + ] + } + }, + "consequent": { + "format": "KORE", + "version": 1, + "term": { + "tag": "And", + "sort": {"tag": "SortApp", "name": "SortInt", "args": []}, + "patterns": [ + {"tag": "EVar", "name": "VarX", "sort": {"tag": "SortApp", "name": "SortInt", "args": []}}, + { + "tag": "Equals", + "argSort": {"tag": "SortApp", "name": "SortBool", "args": []}, + "sort": {"tag": "SortApp", "name": "SortInt", "args": []}, + "first": {"tag": "DV", "sort": {"tag": "SortApp", "name": "SortBool", "args": []}, "value": "true"}, + "second": { + "tag": "App", + "name": "Lbl'Unds-LT-'Int'Unds'", + "sorts": [], + "args": [ + {"tag": "EVar", "name": "VarX", "sort": {"tag": "SortApp", "name": "SortInt", "args": []}}, + {"tag": "DV", "sort": {"tag": "SortApp", "name": "SortInt", "args": []}, "value": "10"} + ] + } + } + ] + } + } + } +} diff --git a/booster/test/rpc-integration/test-implies-smt/state-003-vacuous-antecedent.send b/booster/test/rpc-integration/test-implies-smt/state-003-vacuous-antecedent.send new file mode 100644 index 0000000000..4dd0aa88c3 --- /dev/null +++ b/booster/test/rpc-integration/test-implies-smt/state-003-vacuous-antecedent.send @@ -0,0 +1,75 @@ +{ + "jsonrpc": "2.0", + "id": "implies-smt-003", + "method": "implies", + "params": { + "antecedent": { + "format": "KORE", + "version": 1, + "term": { + "tag": "And", + "sort": {"tag": "SortApp", "name": "SortInt", "args": []}, + "patterns": [ + {"tag": "EVar", "name": "VarX", "sort": {"tag": "SortApp", "name": "SortInt", "args": []}}, + { + "tag": "Equals", + "argSort": {"tag": "SortApp", "name": "SortBool", "args": []}, + "sort": {"tag": "SortApp", "name": "SortInt", "args": []}, + "first": {"tag": "DV", "sort": {"tag": "SortApp", "name": "SortBool", "args": []}, "value": "true"}, + "second": { + "tag": "App", + "name": "Lbl'Unds'andBool'Unds'", + "sorts": [], + "args": [ + { + "tag": "App", + "name": "Lbl'Unds-LT-'Int'Unds'", + "sorts": [], + "args": [ + {"tag": "EVar", "name": "VarX", "sort": {"tag": "SortApp", "name": "SortInt", "args": []}}, + {"tag": "DV", "sort": {"tag": "SortApp", "name": "SortInt", "args": []}, "value": "10"} + ] + }, + { + "tag": "App", + "name": "Lbl'Unds-LT-'Int'Unds'", + "sorts": [], + "args": [ + {"tag": "DV", "sort": {"tag": "SortApp", "name": "SortInt", "args": []}, "value": "20"}, + {"tag": "EVar", "name": "VarX", "sort": {"tag": "SortApp", "name": "SortInt", "args": []}} + ] + } + ] + } + } + ] + } + }, + "consequent": { + "format": "KORE", + "version": 1, + "term": { + "tag": "And", + "sort": {"tag": "SortApp", "name": "SortInt", "args": []}, + "patterns": [ + {"tag": "EVar", "name": "VarX", "sort": {"tag": "SortApp", "name": "SortInt", "args": []}}, + { + "tag": "Equals", + "argSort": {"tag": "SortApp", "name": "SortBool", "args": []}, + "sort": {"tag": "SortApp", "name": "SortInt", "args": []}, + "first": {"tag": "DV", "sort": {"tag": "SortApp", "name": "SortBool", "args": []}, "value": "true"}, + "second": { + "tag": "App", + "name": "Lbl'Unds-LT-'Int'Unds'", + "sorts": [], + "args": [ + {"tag": "EVar", "name": "VarX", "sort": {"tag": "SortApp", "name": "SortInt", "args": []}}, + {"tag": "DV", "sort": {"tag": "SortApp", "name": "SortInt", "args": []}, "value": "1000"} + ] + } + } + ] + } + } + } +} diff --git a/booster/test/rpc-integration/test-implies-smt/state-004-address-bound.send b/booster/test/rpc-integration/test-implies-smt/state-004-address-bound.send new file mode 100644 index 0000000000..366ad10baf --- /dev/null +++ b/booster/test/rpc-integration/test-implies-smt/state-004-address-bound.send @@ -0,0 +1,75 @@ +{ + "jsonrpc": "2.0", + "id": "implies-smt-004", + "method": "implies", + "params": { + "antecedent": { + "format": "KORE", + "version": 1, + "term": { + "tag": "And", + "sort": {"tag": "SortApp", "name": "SortInt", "args": []}, + "patterns": [ + {"tag": "EVar", "name": "VarACCT'Unds'ID", "sort": {"tag": "SortApp", "name": "SortInt", "args": []}}, + { + "tag": "Equals", + "argSort": {"tag": "SortApp", "name": "SortBool", "args": []}, + "sort": {"tag": "SortApp", "name": "SortInt", "args": []}, + "first": {"tag": "DV", "sort": {"tag": "SortApp", "name": "SortBool", "args": []}, "value": "true"}, + "second": { + "tag": "App", + "name": "Lbl'Unds'andBool'Unds'", + "sorts": [], + "args": [ + { + "tag": "App", + "name": "Lbl'Unds-LT-Eqls'Int'Unds'", + "sorts": [], + "args": [ + {"tag": "DV", "sort": {"tag": "SortApp", "name": "SortInt", "args": []}, "value": "0"}, + {"tag": "EVar", "name": "VarACCT'Unds'ID", "sort": {"tag": "SortApp", "name": "SortInt", "args": []}} + ] + }, + { + "tag": "App", + "name": "Lbl'Unds-LT-'Int'Unds'", + "sorts": [], + "args": [ + {"tag": "EVar", "name": "VarACCT'Unds'ID", "sort": {"tag": "SortApp", "name": "SortInt", "args": []}}, + {"tag": "DV", "sort": {"tag": "SortApp", "name": "SortInt", "args": []}, "value": "1461501637330902918203684832716283019655932542976"} + ] + } + ] + } + } + ] + } + }, + "consequent": { + "format": "KORE", + "version": 1, + "term": { + "tag": "And", + "sort": {"tag": "SortApp", "name": "SortInt", "args": []}, + "patterns": [ + {"tag": "EVar", "name": "VarACCT'Unds'ID", "sort": {"tag": "SortApp", "name": "SortInt", "args": []}}, + { + "tag": "Equals", + "argSort": {"tag": "SortApp", "name": "SortBool", "args": []}, + "sort": {"tag": "SortApp", "name": "SortInt", "args": []}, + "first": {"tag": "DV", "sort": {"tag": "SortApp", "name": "SortBool", "args": []}, "value": "true"}, + "second": { + "tag": "App", + "name": "Lbl'Unds-LT-'Int'Unds'", + "sorts": [], + "args": [ + {"tag": "EVar", "name": "VarACCT'Unds'ID", "sort": {"tag": "SortApp", "name": "SortInt", "args": []}}, + {"tag": "DV", "sort": {"tag": "SortApp", "name": "SortInt", "args": []}, "value": "115792089237316195423570985008687907853269984665640564039457584007913129639936"} + ] + } + } + ] + } + } + } +} diff --git a/booster/test/rpc-integration/test-implies-smt/state-005-escalate-indeterminate.send b/booster/test/rpc-integration/test-implies-smt/state-005-escalate-indeterminate.send new file mode 100644 index 0000000000..80d2274e8a --- /dev/null +++ b/booster/test/rpc-integration/test-implies-smt/state-005-escalate-indeterminate.send @@ -0,0 +1,148 @@ +{ + "jsonrpc": "2.0", + "id": "implies-smt-005", + "method": "implies", + "params": { + "antecedent": { + "format": "KORE", + "version": 1, + "term": { + "tag": "And", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + }, + "patterns": [ + { + "tag": "EVar", + "name": "VarX", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + } + }, + { + "tag": "Equals", + "argSort": { + "tag": "SortApp", + "name": "SortBool", + "args": [] + }, + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + }, + "first": { + "tag": "DV", + "sort": { + "tag": "SortApp", + "name": "SortBool", + "args": [] + }, + "value": "true" + }, + "second": { + "tag": "App", + "name": "Lbl'Unds-LT-'Int'Unds'", + "sorts": [], + "args": [ + { + "tag": "EVar", + "name": "VarX", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + } + }, + { + "tag": "DV", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + }, + "value": "100" + } + ] + } + } + ] + } + }, + "consequent": { + "format": "KORE", + "version": 1, + "term": { + "tag": "And", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + }, + "patterns": [ + { + "tag": "EVar", + "name": "VarX", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + } + }, + { + "tag": "Equals", + "argSort": { + "tag": "SortApp", + "name": "SortBool", + "args": [] + }, + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + }, + "first": { + "tag": "DV", + "sort": { + "tag": "SortApp", + "name": "SortBool", + "args": [] + }, + "value": "true" + }, + "second": { + "tag": "App", + "name": "Lbl'Unds-LT-'Int'Unds'", + "sorts": [], + "args": [ + { + "tag": "EVar", + "name": "VarX", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + } + }, + { + "tag": "DV", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + }, + "value": "10" + } + ] + } + } + ] + } + }, + "assume-defined": true + } +} diff --git a/booster/test/rpc-integration/test-implies/response-0->1.json b/booster/test/rpc-integration/test-implies/response-0->1.json index 89f7227f82..fbd010965f 100644 --- a/booster/test/rpc-integration/test-implies/response-0->1.json +++ b/booster/test/rpc-integration/test-implies/response-0->1.json @@ -1 +1 @@ -{"jsonrpc":"2.0","id":"4420705104-001","result":{"valid":false,"implication":{"format":"KORE","version":1,"term":{"tag":"Implies","sort":{"tag":"SortApp","name":"SortInt","args":[]},"first":{"tag":"DV","sort":{"tag":"SortApp","name":"SortInt","args":[]},"value":"0"},"second":{"tag":"DV","sort":{"tag":"SortApp","name":"SortInt","args":[]},"value":"1"}}}}} \ No newline at end of file +{"jsonrpc":"2.0","id":"4420705104-001","result":{"status":"invalid","implication":{"format":"KORE","version":1,"term":{"tag":"Implies","sort":{"tag":"SortApp","name":"SortInt","args":[]},"first":{"tag":"DV","sort":{"tag":"SortApp","name":"SortInt","args":[]},"value":"0"},"second":{"tag":"DV","sort":{"tag":"SortApp","name":"SortInt","args":[]},"value":"1"}}}}} \ No newline at end of file diff --git a/booster/test/rpc-integration/test-implies/response-0->B.json b/booster/test/rpc-integration/test-implies/response-0->B.json index da02aedd1d..1dd1fd0902 100644 --- a/booster/test/rpc-integration/test-implies/response-0->B.json +++ b/booster/test/rpc-integration/test-implies/response-0->B.json @@ -2,7 +2,7 @@ "jsonrpc": "2.0", "id": "4420703856-001", "result": { - "valid": false, + "status": "invalid", "implication": { "format": "KORE", "version": 1, diff --git a/booster/test/rpc-integration/test-implies/response-0->T.json b/booster/test/rpc-integration/test-implies/response-0->T.json index a9be50bb9b..4d78f76328 100644 --- a/booster/test/rpc-integration/test-implies/response-0->T.json +++ b/booster/test/rpc-integration/test-implies/response-0->T.json @@ -1 +1 @@ -{"jsonrpc":"2.0","id":"4420703856-001","result":{"valid":true,"implication":{"format":"KORE","version":1,"term":{"tag":"Implies","sort":{"tag":"SortApp","name":"SortInt","args":[]},"first":{"tag":"DV","sort":{"tag":"SortApp","name":"SortInt","args":[]},"value":"0"},"second":{"tag":"Top","sort":{"tag":"SortApp","name":"SortInt","args":[]}}}},"condition":{"substitution":{"format":"KORE","version":1,"term":{"tag":"Top","sort":{"tag":"SortApp","name":"SortInt","args":[]}}},"predicate":{"format":"KORE","version":1,"term":{"tag":"Top","sort":{"tag":"SortApp","name":"SortInt","args":[]}}}}}} \ No newline at end of file +{"jsonrpc":"2.0","id":"4420703856-001","result":{"status":"valid","implication":{"format":"KORE","version":1,"term":{"tag":"Implies","sort":{"tag":"SortApp","name":"SortInt","args":[]},"first":{"tag":"DV","sort":{"tag":"SortApp","name":"SortInt","args":[]},"value":"0"},"second":{"tag":"Top","sort":{"tag":"SortApp","name":"SortInt","args":[]}}}},"condition":{"substitution":{"format":"KORE","version":1,"term":{"tag":"Top","sort":{"tag":"SortApp","name":"SortInt","args":[]}}},"predicate":{"format":"KORE","version":1,"term":{"tag":"Top","sort":{"tag":"SortApp","name":"SortInt","args":[]}}}}}} \ No newline at end of file diff --git a/booster/test/rpc-integration/test-implies/response-B->0.json b/booster/test/rpc-integration/test-implies/response-B->0.json index d20f9364af..4b8984c689 100644 --- a/booster/test/rpc-integration/test-implies/response-B->0.json +++ b/booster/test/rpc-integration/test-implies/response-B->0.json @@ -2,7 +2,7 @@ "jsonrpc": "2.0", "id": "4420703856-001", "result": { - "valid": true, + "status": "valid", "implication": { "format": "KORE", "version": 1, diff --git a/booster/test/rpc-integration/test-implies/response-X->0.booster-dev b/booster/test/rpc-integration/test-implies/response-X->0.booster-dev index b25a9d8976..92c66f6496 100644 --- a/booster/test/rpc-integration/test-implies/response-X->0.booster-dev +++ b/booster/test/rpc-integration/test-implies/response-X->0.booster-dev @@ -2,7 +2,7 @@ "jsonrpc": "2.0", "id": "4420567456-001", "result": { - "valid": false, + "status": "invalid", "implication": { "format": "KORE", "version": 1, diff --git a/booster/test/rpc-integration/test-implies/response-X->0.json b/booster/test/rpc-integration/test-implies/response-X->0.json index d77c0fed50..21360823ef 100644 --- a/booster/test/rpc-integration/test-implies/response-X->0.json +++ b/booster/test/rpc-integration/test-implies/response-X->0.json @@ -2,7 +2,7 @@ "jsonrpc": "2.0", "id": "4420567456-001", "result": { - "valid": false, + "status": "invalid", "implication": { "format": "KORE", "version": 1, diff --git a/booster/test/rpc-integration/test-implies/response-X->T.json b/booster/test/rpc-integration/test-implies/response-X->T.json index 9751afcafb..93f72cc228 100644 --- a/booster/test/rpc-integration/test-implies/response-X->T.json +++ b/booster/test/rpc-integration/test-implies/response-X->T.json @@ -2,7 +2,7 @@ "jsonrpc": "2.0", "id": "4420498928-001", "result": { - "valid": true, + "status": "valid", "implication": { "format": "KORE", "version": 1, diff --git a/booster/test/rpc-integration/test-implies/response-X->X.json b/booster/test/rpc-integration/test-implies/response-X->X.json index 9aa0c049dd..08b3df1118 100644 --- a/booster/test/rpc-integration/test-implies/response-X->X.json +++ b/booster/test/rpc-integration/test-implies/response-X->X.json @@ -1 +1 @@ -{"jsonrpc":"2.0","id":"4420580224-001","result":{"valid":true,"implication":{"format":"KORE","version":1,"term":{"tag":"Implies","sort":{"tag":"SortApp","name":"SortInt","args":[]},"first":{"tag":"EVar","name":"x","sort":{"tag":"SortApp","name":"SortInt","args":[]}},"second":{"tag":"EVar","name":"x","sort":{"tag":"SortApp","name":"SortInt","args":[]}}}},"condition":{"substitution":{"format":"KORE","version":1,"term":{"tag":"Top","sort":{"tag":"SortApp","name":"SortInt","args":[]}}},"predicate":{"format":"KORE","version":1,"term":{"tag":"Top","sort":{"tag":"SortApp","name":"SortInt","args":[]}}}}}} \ No newline at end of file +{"jsonrpc":"2.0","id":"4420580224-001","result":{"status":"valid","implication":{"format":"KORE","version":1,"term":{"tag":"Implies","sort":{"tag":"SortApp","name":"SortInt","args":[]},"first":{"tag":"EVar","name":"x","sort":{"tag":"SortApp","name":"SortInt","args":[]}},"second":{"tag":"EVar","name":"x","sort":{"tag":"SortApp","name":"SortInt","args":[]}}}},"condition":{"substitution":{"format":"KORE","version":1,"term":{"tag":"Top","sort":{"tag":"SortApp","name":"SortInt","args":[]}}},"predicate":{"format":"KORE","version":1,"term":{"tag":"Top","sort":{"tag":"SortApp","name":"SortInt","args":[]}}}}}} \ No newline at end of file diff --git a/booster/test/rpc-integration/test-implies/response-fail-0->X.json b/booster/test/rpc-integration/test-implies/response-fail-0->X.json index 89f7227f82..fbd010965f 100644 --- a/booster/test/rpc-integration/test-implies/response-fail-0->X.json +++ b/booster/test/rpc-integration/test-implies/response-fail-0->X.json @@ -1 +1 @@ -{"jsonrpc":"2.0","id":"4420705104-001","result":{"valid":false,"implication":{"format":"KORE","version":1,"term":{"tag":"Implies","sort":{"tag":"SortApp","name":"SortInt","args":[]},"first":{"tag":"DV","sort":{"tag":"SortApp","name":"SortInt","args":[]},"value":"0"},"second":{"tag":"DV","sort":{"tag":"SortApp","name":"SortInt","args":[]},"value":"1"}}}}} \ No newline at end of file +{"jsonrpc":"2.0","id":"4420705104-001","result":{"status":"invalid","implication":{"format":"KORE","version":1,"term":{"tag":"Implies","sort":{"tag":"SortApp","name":"SortInt","args":[]},"first":{"tag":"DV","sort":{"tag":"SortApp","name":"SortInt","args":[]},"value":"0"},"second":{"tag":"DV","sort":{"tag":"SortApp","name":"SortInt","args":[]},"value":"1"}}}}} \ No newline at end of file diff --git a/booster/test/rpc-integration/test-implies2/response-antecedent-bottom.json b/booster/test/rpc-integration/test-implies2/response-antecedent-bottom.json index 2273a73cdc..5d8ab14557 100644 --- a/booster/test/rpc-integration/test-implies2/response-antecedent-bottom.json +++ b/booster/test/rpc-integration/test-implies2/response-antecedent-bottom.json @@ -2,7 +2,7 @@ "jsonrpc": "2.0", "id": "4428382960-001", "result": { - "valid": true, + "status": "valid", "implication": { "format": "KORE", "version": 1, diff --git a/booster/test/rpc-integration/test-implies2/response-consequent-constraint.booster-dev b/booster/test/rpc-integration/test-implies2/response-consequent-constraint.booster-dev index 3f95ef2531..f77c8a295a 100644 --- a/booster/test/rpc-integration/test-implies2/response-consequent-constraint.booster-dev +++ b/booster/test/rpc-integration/test-implies2/response-consequent-constraint.booster-dev @@ -1,9 +1,357 @@ { "jsonrpc": "2.0", "id": "4567908768-001", - "error": { - "code": 6, - "data": "unknown constraints", - "message": "Aborted" + "result": { + "status": "indeterminate", + "implication": { + "format": "KORE", + "version": 1, + "term": { + "tag": "Implies", + "sort": { + "tag": "SortApp", + "name": "SortGeneratedTopCell", + "args": [] + }, + "first": { + "tag": "App", + "name": "Lbl'-LT-'generatedTop'-GT-'", + "sorts": [], + "args": [ + { + "tag": "App", + "name": "Lbl'-LT-'T'-GT-'", + "sorts": [], + "args": [ + { + "tag": "App", + "name": "Lbl'-LT-'k'-GT-'", + "sorts": [], + "args": [ + { + "tag": "App", + "name": "kseq", + "sorts": [], + "args": [ + { + "tag": "App", + "name": "inj", + "sorts": [ + { + "tag": "SortApp", + "name": "SortPgm", + "args": [] + }, + { + "tag": "SortApp", + "name": "SortKItem", + "args": [] + } + ], + "args": [ + { + "tag": "App", + "name": "Lblint'UndsSClnUnds'", + "sorts": [], + "args": [ + { + "tag": "App", + "name": "Lbl'UndsCommUnds'", + "sorts": [], + "args": [ + { + "tag": "DV", + "sort": { + "tag": "SortApp", + "name": "SortId", + "args": [] + }, + "value": "$n" + }, + { + "tag": "App", + "name": "Lbl'UndsCommUnds'", + "sorts": [], + "args": [ + { + "tag": "DV", + "sort": { + "tag": "SortApp", + "name": "SortId", + "args": [] + }, + "value": "$s" + }, + { + "tag": "App", + "name": "Lbl'Stop'List'LBraQuotUndsCommUndsQuotRBra'", + "sorts": [], + "args": [] + } + ] + } + ] + }, + { + "tag": "App", + "name": "Lbl'UndsEqlsUndsSCln'", + "sorts": [], + "args": [ + { + "tag": "DV", + "sort": { + "tag": "SortApp", + "name": "SortId", + "args": [] + }, + "value": "$n" + }, + { + "tag": "App", + "name": "inj", + "sorts": [ + { + "tag": "SortApp", + "name": "SortInt", + "args": [] + }, + { + "tag": "SortApp", + "name": "SortAExp", + "args": [] + } + ], + "args": [ + { + "tag": "DV", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + }, + "value": "3" + } + ] + } + ] + } + ] + } + ] + }, + { + "tag": "App", + "name": "dotk", + "sorts": [], + "args": [] + } + ] + } + ] + }, + { + "tag": "App", + "name": "Lbl'-LT-'state'-GT-'", + "sorts": [], + "args": [ + { + "tag": "App", + "name": "Lbl'Stop'Map", + "sorts": [], + "args": [] + } + ] + } + ] + }, + { + "tag": "EVar", + "name": "VarGENERATED'Unds'COUNTER'Unds'CELL", + "sort": { + "tag": "SortApp", + "name": "SortGeneratedCounterCell", + "args": [] + } + } + ] + }, + "second": { + "tag": "Exists", + "sort": { + "tag": "SortApp", + "name": "SortGeneratedTopCell", + "args": [] + }, + "var": "VarX", + "varSort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + }, + "arg": { + "tag": "App", + "name": "Lbl'-LT-'generatedTop'-GT-'", + "sorts": [], + "args": [ + { + "tag": "App", + "name": "Lbl'-LT-'T'-GT-'", + "sorts": [], + "args": [ + { + "tag": "App", + "name": "Lbl'-LT-'k'-GT-'", + "sorts": [], + "args": [ + { + "tag": "App", + "name": "kseq", + "sorts": [], + "args": [ + { + "tag": "App", + "name": "inj", + "sorts": [ + { + "tag": "SortApp", + "name": "SortPgm", + "args": [] + }, + { + "tag": "SortApp", + "name": "SortKItem", + "args": [] + } + ], + "args": [ + { + "tag": "App", + "name": "Lblint'UndsSClnUnds'", + "sorts": [], + "args": [ + { + "tag": "App", + "name": "Lbl'UndsCommUnds'", + "sorts": [], + "args": [ + { + "tag": "DV", + "sort": { + "tag": "SortApp", + "name": "SortId", + "args": [] + }, + "value": "$n" + }, + { + "tag": "App", + "name": "Lbl'UndsCommUnds'", + "sorts": [], + "args": [ + { + "tag": "DV", + "sort": { + "tag": "SortApp", + "name": "SortId", + "args": [] + }, + "value": "$s" + }, + { + "tag": "App", + "name": "Lbl'Stop'List'LBraQuotUndsCommUndsQuotRBra'", + "sorts": [], + "args": [] + } + ] + } + ] + }, + { + "tag": "App", + "name": "Lbl'UndsEqlsUndsSCln'", + "sorts": [], + "args": [ + { + "tag": "DV", + "sort": { + "tag": "SortApp", + "name": "SortId", + "args": [] + }, + "value": "$n" + }, + { + "tag": "App", + "name": "inj", + "sorts": [ + { + "tag": "SortApp", + "name": "SortInt", + "args": [] + }, + { + "tag": "SortApp", + "name": "SortAExp", + "args": [] + } + ], + "args": [ + { + "tag": "EVar", + "name": "VarX", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + } + } + ] + } + ] + } + ] + } + ] + }, + { + "tag": "App", + "name": "dotk", + "sorts": [], + "args": [] + } + ] + } + ] + }, + { + "tag": "App", + "name": "Lbl'-LT-'state'-GT-'", + "sorts": [], + "args": [ + { + "tag": "App", + "name": "Lbl'Stop'Map", + "sorts": [], + "args": [] + } + ] + } + ] + }, + { + "tag": "EVar", + "name": "VarGENERATED'Unds'COUNTER'Unds'CELL", + "sort": { + "tag": "SortApp", + "name": "SortGeneratedCounterCell", + "args": [] + } + } + ] + } + } + } + } } } \ No newline at end of file diff --git a/booster/test/rpc-integration/test-implies2/response-consequent-constraint.json b/booster/test/rpc-integration/test-implies2/response-consequent-constraint.json index 3f535300d0..48c3c914a5 100644 --- a/booster/test/rpc-integration/test-implies2/response-consequent-constraint.json +++ b/booster/test/rpc-integration/test-implies2/response-consequent-constraint.json @@ -2,7 +2,7 @@ "jsonrpc": "2.0", "id": "4567908768-001", "result": { - "valid": false, + "status": "invalid", "implication": { "format": "KORE", "version": 1, diff --git a/booster/test/rpc-integration/test-implies2/response-constant-subst.json b/booster/test/rpc-integration/test-implies2/response-constant-subst.json index 7ad036dd1b..5806b24487 100644 --- a/booster/test/rpc-integration/test-implies2/response-constant-subst.json +++ b/booster/test/rpc-integration/test-implies2/response-constant-subst.json @@ -2,7 +2,7 @@ "jsonrpc": "2.0", "id": "4567924032-001", "result": { - "valid": true, + "status": "valid", "implication": { "format": "KORE", "version": 1, diff --git a/booster/test/rpc-integration/test-implies2/response-refutation-1.booster-dev b/booster/test/rpc-integration/test-implies2/response-refutation-1.booster-dev index 06ff97f484..df595f9aec 100644 --- a/booster/test/rpc-integration/test-implies2/response-refutation-1.booster-dev +++ b/booster/test/rpc-integration/test-implies2/response-refutation-1.booster-dev @@ -1,9 +1,325 @@ { "jsonrpc": "2.0", "id": "4428832288-001", - "error": { - "code": 6, - "data": "unknown constraints", - "message": "Aborted" + "result": { + "status": "indeterminate", + "implication": { + "format": "KORE", + "version": 1, + "term": { + "tag": "Implies", + "sort": { + "tag": "SortApp", + "name": "SortGeneratedTopCell", + "args": [] + }, + "first": { + "tag": "App", + "name": "Lbl'-LT-'generatedTop'-GT-'", + "sorts": [], + "args": [ + { + "tag": "App", + "name": "Lbl'-LT-'T'-GT-'", + "sorts": [], + "args": [ + { + "tag": "App", + "name": "Lbl'-LT-'k'-GT-'", + "sorts": [], + "args": [ + { + "tag": "App", + "name": "kseq", + "sorts": [], + "args": [ + { + "tag": "App", + "name": "inj", + "sorts": [ + { + "tag": "SortApp", + "name": "SortPgm", + "args": [] + }, + { + "tag": "SortApp", + "name": "SortKItem", + "args": [] + } + ], + "args": [ + { + "tag": "App", + "name": "Lblint'UndsSClnUnds'", + "sorts": [], + "args": [ + { + "tag": "App", + "name": "Lbl'UndsCommUnds'", + "sorts": [], + "args": [ + { + "tag": "DV", + "sort": { + "tag": "SortApp", + "name": "SortId", + "args": [] + }, + "value": "$n" + }, + { + "tag": "App", + "name": "Lbl'Stop'List'LBraQuotUndsCommUndsQuotRBra'", + "sorts": [], + "args": [] + } + ] + }, + { + "tag": "App", + "name": "Lbl'UndsEqlsUndsSCln'", + "sorts": [], + "args": [ + { + "tag": "DV", + "sort": { + "tag": "SortApp", + "name": "SortId", + "args": [] + }, + "value": "$n" + }, + { + "tag": "App", + "name": "inj", + "sorts": [ + { + "tag": "SortApp", + "name": "SortInt", + "args": [] + }, + { + "tag": "SortApp", + "name": "SortAExp", + "args": [] + } + ], + "args": [ + { + "tag": "DV", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + }, + "value": "0" + } + ] + } + ] + } + ] + } + ] + }, + { + "tag": "App", + "name": "dotk", + "sorts": [], + "args": [] + } + ] + } + ] + }, + { + "tag": "App", + "name": "Lbl'-LT-'state'-GT-'", + "sorts": [], + "args": [ + { + "tag": "App", + "name": "Lbl'Stop'Map", + "sorts": [], + "args": [] + } + ] + } + ] + }, + { + "tag": "EVar", + "name": "VarGENERATED'Unds'COUNTER'Unds'CELL", + "sort": { + "tag": "SortApp", + "name": "SortGeneratedCounterCell", + "args": [] + } + } + ] + }, + "second": { + "tag": "Exists", + "sort": { + "tag": "SortApp", + "name": "SortGeneratedTopCell", + "args": [] + }, + "var": "VarX", + "varSort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + }, + "arg": { + "tag": "App", + "name": "Lbl'-LT-'generatedTop'-GT-'", + "sorts": [], + "args": [ + { + "tag": "App", + "name": "Lbl'-LT-'T'-GT-'", + "sorts": [], + "args": [ + { + "tag": "App", + "name": "Lbl'-LT-'k'-GT-'", + "sorts": [], + "args": [ + { + "tag": "App", + "name": "kseq", + "sorts": [], + "args": [ + { + "tag": "App", + "name": "inj", + "sorts": [ + { + "tag": "SortApp", + "name": "SortPgm", + "args": [] + }, + { + "tag": "SortApp", + "name": "SortKItem", + "args": [] + } + ], + "args": [ + { + "tag": "App", + "name": "Lblint'UndsSClnUnds'", + "sorts": [], + "args": [ + { + "tag": "App", + "name": "Lbl'UndsCommUnds'", + "sorts": [], + "args": [ + { + "tag": "DV", + "sort": { + "tag": "SortApp", + "name": "SortId", + "args": [] + }, + "value": "$n" + }, + { + "tag": "App", + "name": "Lbl'Stop'List'LBraQuotUndsCommUndsQuotRBra'", + "sorts": [], + "args": [] + } + ] + }, + { + "tag": "App", + "name": "Lbl'UndsEqlsUndsSCln'", + "sorts": [], + "args": [ + { + "tag": "DV", + "sort": { + "tag": "SortApp", + "name": "SortId", + "args": [] + }, + "value": "$n" + }, + { + "tag": "App", + "name": "inj", + "sorts": [ + { + "tag": "SortApp", + "name": "SortInt", + "args": [] + }, + { + "tag": "SortApp", + "name": "SortAExp", + "args": [] + } + ], + "args": [ + { + "tag": "DV", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + }, + "value": "0" + } + ] + } + ] + } + ] + } + ] + }, + { + "tag": "App", + "name": "dotk", + "sorts": [], + "args": [] + } + ] + } + ] + }, + { + "tag": "App", + "name": "Lbl'-LT-'state'-GT-'", + "sorts": [], + "args": [ + { + "tag": "App", + "name": "Lbl'Stop'Map", + "sorts": [], + "args": [] + } + ] + } + ] + }, + { + "tag": "EVar", + "name": "VarGENERATED'Unds'COUNTER'Unds'CELL", + "sort": { + "tag": "SortApp", + "name": "SortGeneratedCounterCell", + "args": [] + } + } + ] + } + } + } + } } } \ No newline at end of file diff --git a/booster/test/rpc-integration/test-implies2/response-refutation-1.json b/booster/test/rpc-integration/test-implies2/response-refutation-1.json index f99fa6258f..da1e3e547f 100644 --- a/booster/test/rpc-integration/test-implies2/response-refutation-1.json +++ b/booster/test/rpc-integration/test-implies2/response-refutation-1.json @@ -2,7 +2,7 @@ "jsonrpc": "2.0", "id": "4428832288-001", "result": { - "valid": true, + "status": "valid", "implication": { "format": "KORE", "version": 1, diff --git a/booster/test/rpc-integration/test-implies2/response-refutation-3.booster-dev b/booster/test/rpc-integration/test-implies2/response-refutation-3.booster-dev index 6567ec123d..e5de7a24ed 100644 --- a/booster/test/rpc-integration/test-implies2/response-refutation-3.booster-dev +++ b/booster/test/rpc-integration/test-implies2/response-refutation-3.booster-dev @@ -1,9 +1,339 @@ { "jsonrpc": "2.0", "id": "4573738480-001", - "error": { - "code": 6, - "data": "unknown constraints", - "message": "Aborted" + "result": { + "status": "indeterminate", + "implication": { + "format": "KORE", + "version": 1, + "term": { + "tag": "Implies", + "sort": { + "tag": "SortApp", + "name": "SortGeneratedTopCell", + "args": [] + }, + "first": { + "tag": "App", + "name": "Lbl'-LT-'generatedTop'-GT-'", + "sorts": [], + "args": [ + { + "tag": "App", + "name": "Lbl'-LT-'T'-GT-'", + "sorts": [], + "args": [ + { + "tag": "App", + "name": "Lbl'-LT-'k'-GT-'", + "sorts": [], + "args": [ + { + "tag": "App", + "name": "kseq", + "sorts": [], + "args": [ + { + "tag": "App", + "name": "inj", + "sorts": [ + { + "tag": "SortApp", + "name": "SortPgm", + "args": [] + }, + { + "tag": "SortApp", + "name": "SortKItem", + "args": [] + } + ], + "args": [ + { + "tag": "App", + "name": "Lblint'UndsSClnUnds'", + "sorts": [], + "args": [ + { + "tag": "App", + "name": "Lbl'UndsCommUnds'", + "sorts": [], + "args": [ + { + "tag": "DV", + "sort": { + "tag": "SortApp", + "name": "SortId", + "args": [] + }, + "value": "$n" + }, + { + "tag": "App", + "name": "Lbl'Stop'List'LBraQuotUndsCommUndsQuotRBra'", + "sorts": [], + "args": [] + } + ] + }, + { + "tag": "App", + "name": "Lbl'UndsEqlsUndsSCln'", + "sorts": [], + "args": [ + { + "tag": "DV", + "sort": { + "tag": "SortApp", + "name": "SortId", + "args": [] + }, + "value": "$n" + }, + { + "tag": "App", + "name": "inj", + "sorts": [ + { + "tag": "SortApp", + "name": "SortInt", + "args": [] + }, + { + "tag": "SortApp", + "name": "SortAExp", + "args": [] + } + ], + "args": [ + { + "tag": "DV", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + }, + "value": "0" + } + ] + } + ] + } + ] + } + ] + }, + { + "tag": "App", + "name": "dotk", + "sorts": [], + "args": [] + } + ] + } + ] + }, + { + "tag": "App", + "name": "Lbl'-LT-'state'-GT-'", + "sorts": [], + "args": [ + { + "tag": "App", + "name": "Lbl'Stop'Map", + "sorts": [], + "args": [] + } + ] + } + ] + }, + { + "tag": "EVar", + "name": "VarGENERATED'Unds'COUNTER'Unds'CELL", + "sort": { + "tag": "SortApp", + "name": "SortGeneratedCounterCell", + "args": [] + } + } + ] + }, + "second": { + "tag": "Exists", + "sort": { + "tag": "SortApp", + "name": "SortGeneratedTopCell", + "args": [] + }, + "var": "VarY", + "varSort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + }, + "arg": { + "tag": "Exists", + "sort": { + "tag": "SortApp", + "name": "SortGeneratedTopCell", + "args": [] + }, + "var": "VarX", + "varSort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + }, + "arg": { + "tag": "App", + "name": "Lbl'-LT-'generatedTop'-GT-'", + "sorts": [], + "args": [ + { + "tag": "App", + "name": "Lbl'-LT-'T'-GT-'", + "sorts": [], + "args": [ + { + "tag": "App", + "name": "Lbl'-LT-'k'-GT-'", + "sorts": [], + "args": [ + { + "tag": "App", + "name": "kseq", + "sorts": [], + "args": [ + { + "tag": "App", + "name": "inj", + "sorts": [ + { + "tag": "SortApp", + "name": "SortPgm", + "args": [] + }, + { + "tag": "SortApp", + "name": "SortKItem", + "args": [] + } + ], + "args": [ + { + "tag": "App", + "name": "Lblint'UndsSClnUnds'", + "sorts": [], + "args": [ + { + "tag": "App", + "name": "Lbl'UndsCommUnds'", + "sorts": [], + "args": [ + { + "tag": "DV", + "sort": { + "tag": "SortApp", + "name": "SortId", + "args": [] + }, + "value": "$n" + }, + { + "tag": "App", + "name": "Lbl'Stop'List'LBraQuotUndsCommUndsQuotRBra'", + "sorts": [], + "args": [] + } + ] + }, + { + "tag": "App", + "name": "Lbl'UndsEqlsUndsSCln'", + "sorts": [], + "args": [ + { + "tag": "DV", + "sort": { + "tag": "SortApp", + "name": "SortId", + "args": [] + }, + "value": "$n" + }, + { + "tag": "App", + "name": "inj", + "sorts": [ + { + "tag": "SortApp", + "name": "SortInt", + "args": [] + }, + { + "tag": "SortApp", + "name": "SortAExp", + "args": [] + } + ], + "args": [ + { + "tag": "DV", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + }, + "value": "0" + } + ] + } + ] + } + ] + } + ] + }, + { + "tag": "App", + "name": "dotk", + "sorts": [], + "args": [] + } + ] + } + ] + }, + { + "tag": "App", + "name": "Lbl'-LT-'state'-GT-'", + "sorts": [], + "args": [ + { + "tag": "App", + "name": "Lbl'Stop'Map", + "sorts": [], + "args": [] + } + ] + } + ] + }, + { + "tag": "EVar", + "name": "VarGENERATED'Unds'COUNTER'Unds'CELL", + "sort": { + "tag": "SortApp", + "name": "SortGeneratedCounterCell", + "args": [] + } + } + ] + } + } + } + } + } } } \ No newline at end of file diff --git a/booster/test/rpc-integration/test-implies2/response-refutation-3.json b/booster/test/rpc-integration/test-implies2/response-refutation-3.json index b1f0d44285..f0f05f6e86 100644 --- a/booster/test/rpc-integration/test-implies2/response-refutation-3.json +++ b/booster/test/rpc-integration/test-implies2/response-refutation-3.json @@ -2,7 +2,7 @@ "jsonrpc": "2.0", "id": "4573738480-001", "result": { - "valid": true, + "status": "valid", "implication": { "format": "KORE", "version": 1, diff --git a/booster/test/rpc-integration/test-implies2/response-refutation-4.booster-dev b/booster/test/rpc-integration/test-implies2/response-refutation-4.booster-dev index 31122dc7da..5027122db1 100644 --- a/booster/test/rpc-integration/test-implies2/response-refutation-4.booster-dev +++ b/booster/test/rpc-integration/test-implies2/response-refutation-4.booster-dev @@ -1,9 +1,353 @@ { "jsonrpc": "2.0", "id": "4567922016-001", - "error": { - "code": 6, - "data": "unknown constraints", - "message": "Aborted" + "result": { + "status": "invalid", + "implication": { + "format": "KORE", + "version": 1, + "term": { + "tag": "Implies", + "sort": { + "tag": "SortApp", + "name": "SortGeneratedTopCell", + "args": [] + }, + "first": { + "tag": "App", + "name": "Lbl'-LT-'generatedTop'-GT-'", + "sorts": [], + "args": [ + { + "tag": "App", + "name": "Lbl'-LT-'T'-GT-'", + "sorts": [], + "args": [ + { + "tag": "App", + "name": "Lbl'-LT-'k'-GT-'", + "sorts": [], + "args": [ + { + "tag": "App", + "name": "kseq", + "sorts": [], + "args": [ + { + "tag": "App", + "name": "inj", + "sorts": [ + { + "tag": "SortApp", + "name": "SortPgm", + "args": [] + }, + { + "tag": "SortApp", + "name": "SortKItem", + "args": [] + } + ], + "args": [ + { + "tag": "App", + "name": "Lblint'UndsSClnUnds'", + "sorts": [], + "args": [ + { + "tag": "App", + "name": "Lbl'UndsCommUnds'", + "sorts": [], + "args": [ + { + "tag": "DV", + "sort": { + "tag": "SortApp", + "name": "SortId", + "args": [] + }, + "value": "$n" + }, + { + "tag": "App", + "name": "Lbl'Stop'List'LBraQuotUndsCommUndsQuotRBra'", + "sorts": [], + "args": [] + } + ] + }, + { + "tag": "App", + "name": "Lbl'UndsEqlsUndsSCln'", + "sorts": [], + "args": [ + { + "tag": "DV", + "sort": { + "tag": "SortApp", + "name": "SortId", + "args": [] + }, + "value": "$n" + }, + { + "tag": "App", + "name": "inj", + "sorts": [ + { + "tag": "SortApp", + "name": "SortInt", + "args": [] + }, + { + "tag": "SortApp", + "name": "SortAExp", + "args": [] + } + ], + "args": [ + { + "tag": "DV", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + }, + "value": "0" + } + ] + } + ] + } + ] + } + ] + }, + { + "tag": "App", + "name": "dotk", + "sorts": [], + "args": [] + } + ] + } + ] + }, + { + "tag": "App", + "name": "Lbl'-LT-'state'-GT-'", + "sorts": [], + "args": [ + { + "tag": "App", + "name": "Lbl'Stop'Map", + "sorts": [], + "args": [] + } + ] + } + ] + }, + { + "tag": "EVar", + "name": "VarGENERATED'Unds'COUNTER'Unds'CELL", + "sort": { + "tag": "SortApp", + "name": "SortGeneratedCounterCell", + "args": [] + } + } + ] + }, + "second": { + "tag": "Exists", + "sort": { + "tag": "SortApp", + "name": "SortGeneratedTopCell", + "args": [] + }, + "var": "VarZ", + "varSort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + }, + "arg": { + "tag": "Exists", + "sort": { + "tag": "SortApp", + "name": "SortGeneratedTopCell", + "args": [] + }, + "var": "VarY", + "varSort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + }, + "arg": { + "tag": "Exists", + "sort": { + "tag": "SortApp", + "name": "SortGeneratedTopCell", + "args": [] + }, + "var": "VarX", + "varSort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + }, + "arg": { + "tag": "App", + "name": "Lbl'-LT-'generatedTop'-GT-'", + "sorts": [], + "args": [ + { + "tag": "App", + "name": "Lbl'-LT-'T'-GT-'", + "sorts": [], + "args": [ + { + "tag": "App", + "name": "Lbl'-LT-'k'-GT-'", + "sorts": [], + "args": [ + { + "tag": "App", + "name": "kseq", + "sorts": [], + "args": [ + { + "tag": "App", + "name": "inj", + "sorts": [ + { + "tag": "SortApp", + "name": "SortPgm", + "args": [] + }, + { + "tag": "SortApp", + "name": "SortKItem", + "args": [] + } + ], + "args": [ + { + "tag": "App", + "name": "Lblint'UndsSClnUnds'", + "sorts": [], + "args": [ + { + "tag": "App", + "name": "Lbl'UndsCommUnds'", + "sorts": [], + "args": [ + { + "tag": "DV", + "sort": { + "tag": "SortApp", + "name": "SortId", + "args": [] + }, + "value": "$n" + }, + { + "tag": "App", + "name": "Lbl'Stop'List'LBraQuotUndsCommUndsQuotRBra'", + "sorts": [], + "args": [] + } + ] + }, + { + "tag": "App", + "name": "Lbl'UndsEqlsUndsSCln'", + "sorts": [], + "args": [ + { + "tag": "DV", + "sort": { + "tag": "SortApp", + "name": "SortId", + "args": [] + }, + "value": "$n" + }, + { + "tag": "App", + "name": "inj", + "sorts": [ + { + "tag": "SortApp", + "name": "SortInt", + "args": [] + }, + { + "tag": "SortApp", + "name": "SortAExp", + "args": [] + } + ], + "args": [ + { + "tag": "DV", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + }, + "value": "0" + } + ] + } + ] + } + ] + } + ] + }, + { + "tag": "App", + "name": "dotk", + "sorts": [], + "args": [] + } + ] + } + ] + }, + { + "tag": "App", + "name": "Lbl'-LT-'state'-GT-'", + "sorts": [], + "args": [ + { + "tag": "App", + "name": "Lbl'Stop'Map", + "sorts": [], + "args": [] + } + ] + } + ] + }, + { + "tag": "EVar", + "name": "VarGENERATED'Unds'COUNTER'Unds'CELL", + "sort": { + "tag": "SortApp", + "name": "SortGeneratedCounterCell", + "args": [] + } + } + ] + } + } + } + } + } + } } } \ No newline at end of file diff --git a/booster/test/rpc-integration/test-implies2/response-refutation-4.json b/booster/test/rpc-integration/test-implies2/response-refutation-4.json index 1b3bcc5aa8..3a785c5830 100644 --- a/booster/test/rpc-integration/test-implies2/response-refutation-4.json +++ b/booster/test/rpc-integration/test-implies2/response-refutation-4.json @@ -2,7 +2,7 @@ "jsonrpc": "2.0", "id": "4567922016-001", "result": { - "valid": false, + "status": "invalid", "implication": { "format": "KORE", "version": 1, diff --git a/booster/test/rpc-integration/test-implies2/response-trivial.json b/booster/test/rpc-integration/test-implies2/response-trivial.json index 32408417d5..ddc2d02be9 100644 --- a/booster/test/rpc-integration/test-implies2/response-trivial.json +++ b/booster/test/rpc-integration/test-implies2/response-trivial.json @@ -2,7 +2,7 @@ "jsonrpc": "2.0", "id": "4568002640-001", "result": { - "valid": true, + "status": "valid", "implication": { "format": "KORE", "version": 1, diff --git a/booster/test/rpc-integration/test-implies2/response-variable-subst.json b/booster/test/rpc-integration/test-implies2/response-variable-subst.json index 694e50fc26..2d9e2684b8 100644 --- a/booster/test/rpc-integration/test-implies2/response-variable-subst.json +++ b/booster/test/rpc-integration/test-implies2/response-variable-subst.json @@ -2,7 +2,7 @@ "jsonrpc": "2.0", "id": "4428840880-001", "result": { - "valid": true, + "status": "valid", "implication": { "format": "KORE", "version": 1, diff --git a/booster/tools/booster/Proxy.hs b/booster/tools/booster/Proxy.hs index 2be6308e72..3bbc2349ad 100644 --- a/booster/tools/booster/Proxy.hs +++ b/booster/tools/booster/Proxy.hs @@ -182,7 +182,34 @@ respondEither cfg@ProxyConfig{boosterState, koreCaptureRegistry} booster kore re | fromMaybe False impliesReq.assumeDefined || fromMaybe False impliesReq.boosterOnly -> do -- try the booster end-point first (boosterResult, boosterTime) <- Stats.timed $ booster req + let koreImpliesFallback reason = do + Booster.Log.withContext CtxProxy $ + Booster.Log.logMessage (reason :: Text) + (koreRes, koreTime) <- Stats.timed $ kore req + logStats ImpliesM (boosterTime + koreTime, koreTime) + Booster.Log.withContexts [CtxProxy, CtxAbort, CtxDetail] $ + Booster.Log.logMessage $ + WithJsonMessage + ( object $ + [ "tag" .= ("kore-implies-fallback" :: Text) + , "antecedent" .= impliesReq.antecedent + , "consequent" .= impliesReq.consequent + ] + <> case koreRes of + Right (Implies r) -> ["status" .= r.status] + _ -> [] + ) + ("kore-implies-fallback" :: Text) + pure koreRes case boosterResult of + -- Booster could not decide (indeterminate match / SMT-unknown + -- obligation): escalate to kore so the check still gets a + -- decisive answer. Skipped under booster-only, where the + -- indeterminate result is returned as-is for the client to act on. + Right (Implies r) + | r.status == Indeterminate + , not (fromMaybe False impliesReq.boosterOnly) -> + koreImpliesFallback "Implies indeterminate in booster. Falling back to kore." res@Right{} -> do logStats ImpliesM (boosterTime, 0) pure res @@ -210,28 +237,9 @@ respondEither cfg@ProxyConfig{boosterState, koreCaptureRegistry} booster kore re ("booster-implies-invalid" :: Text) logStats ImpliesM (boosterTime, 0) pure $ Left err - | otherwise -> do - Booster.Log.withContext CtxProxy $ - Booster.Log.logMessage . Text.pack $ - "Implies abort in booster: " - <> fromError err - <> ". Falling back to kore." - (koreRes, koreTime) <- Stats.timed $ kore req - logStats ImpliesM (boosterTime + koreTime, koreTime) - Booster.Log.withContexts [CtxProxy, CtxAbort, CtxDetail] $ - Booster.Log.logMessage $ - WithJsonMessage - ( object $ - [ "tag" .= ("kore-implies-fallback" :: Text) - , "antecedent" .= impliesReq.antecedent - , "consequent" .= impliesReq.consequent - ] - <> case koreRes of - Right (Implies r) -> ["valid" .= r.valid] - _ -> [] - ) - ("kore-implies-fallback" :: Text) - pure koreRes + | otherwise -> + koreImpliesFallback . Text.pack $ + "Implies abort in booster: " <> fromError err <> ". Falling back to kore." | otherwise -> do (koreRes, koreTime) <- Stats.timed $ kore req logStats ImpliesM (koreTime, koreTime) @@ -245,7 +253,7 @@ respondEither cfg@ProxyConfig{boosterState, koreCaptureRegistry} booster kore re , "consequent" .= impliesReq.consequent ] <> case koreRes of - Right (Implies r) -> ["valid" .= r.valid] + Right (Implies r) -> ["status" .= r.status] _ -> [] ) ("kore-implies" :: Text) diff --git a/kore-rpc-types/src/Kore/JsonRpc/Types.hs b/kore-rpc-types/src/Kore/JsonRpc/Types.hs index 0716971038..167466db15 100644 --- a/kore-rpc-types/src/Kore/JsonRpc/Types.hs +++ b/kore-rpc-types/src/Kore/JsonRpc/Types.hs @@ -164,9 +164,28 @@ data Condition = Condition (FromJSON, ToJSON) via CustomJSON '[OmitNothingFields, FieldLabelModifier '[CamelToKebab]] Condition +-- | Tri-state verdict of an implication check. +data ImpliesStatus + = -- | The implication holds (the witnessing substitution / predicate is + -- carried in 'ImpliesResult.condition'). + Valid + | -- | The implication decisively does not hold (a 'MatchFailed{}', an + -- SMT-refuted consequent obligation, or a bottom consequent). + Invalid + | -- | Booster could not decide: its match check was indeterminate (e.g. + -- an unevaluated function blocking unification) and the simplify / + -- SMT-discharge ladder did not settle the obligations. A recover-mode + -- client should escalate to kore rather than trust the result. Kore + -- checks are always decisive and never produce this. + Indeterminate + deriving stock (Generic, Show, Eq) + deriving + (FromJSON, ToJSON) + via CustomJSON '[OmitNothingFields, ConstructorTagModifier '[CamelToKebab]] ImpliesStatus + data ImpliesResult = ImpliesResult { implication :: KoreJson - , valid :: Bool + , status :: ImpliesStatus , condition :: Maybe Condition , logs :: Maybe [LogEntry] , haskellLogEntries :: Maybe [LogLine] diff --git a/kore/src/Kore/JsonRpc.hs b/kore/src/Kore/JsonRpc.hs index a568cd8e52..886845ceef 100644 --- a/kore/src/Kore/JsonRpc.hs +++ b/kore/src/Kore/JsonRpc.hs @@ -470,16 +470,16 @@ respond reqId serverState moduleName runSMT = in Right . Implies $ case r of Claim.Implied Nothing -> - ImpliesResult jsonTerm True (Just . renderCond sort $ Condition.bottom) logs Nothing + ImpliesResult jsonTerm Valid (Just . renderCond sort $ Condition.bottom) logs Nothing Claim.Implied (Just cond) -> - ImpliesResult jsonTerm True (Just . renderCond sort $ cond) logs Nothing + ImpliesResult jsonTerm Valid (Just . renderCond sort $ cond) logs Nothing Claim.NotImplied _ -> - ImpliesResult jsonTerm False Nothing logs Nothing + ImpliesResult jsonTerm Invalid Nothing logs Nothing Claim.NotImpliedStuck (Just cond) -> let jsonCond = renderCond sort cond - in ImpliesResult jsonTerm False (Just jsonCond) logs Nothing + in ImpliesResult jsonTerm Invalid (Just jsonCond) logs Nothing Claim.NotImpliedStuck Nothing -> - ImpliesResult jsonTerm False (Just . renderCond sort $ Condition.bottom) logs Nothing + ImpliesResult jsonTerm Invalid (Just . renderCond sort $ Condition.bottom) logs Nothing Simplify SimplifyRequest{state, _module} -> withMainModule (coerce _module) $ \serializedModule lemmas -> do case verifyIn serializedModule state of Left Error{errorError, errorContext} -> diff --git a/scripts/booster-integration-tests.sh b/scripts/booster-integration-tests.sh index 7cae5fe783..4a60246bb6 100755 --- a/scripts/booster-integration-tests.sh +++ b/scripts/booster-integration-tests.sh @@ -37,7 +37,7 @@ for dir in $(ls -d test-*); do SERVER=$KORE_RPC_DEV ./runDirectoryTest.sh test-$name $@ SERVER=$KORE_RPC_BOOSTER ./runDirectoryTest.sh test-$name $@ ;; - "get-model" | "collectiontest" | "implies" | "implies2" | "implies-issue-3941" | "remainder-predicates" | "use-path-condition-in-equations" | "issue3764-vacuous-branch" | "3934-smt") + "get-model" | "collectiontest" | "implies" | "implies2" | "implies-issue-3941" | "implies-smt" | "remainder-predicates" | "use-path-condition-in-equations" | "issue3764-vacuous-branch" | "3934-smt") SERVER=$BOOSTER_DEV ./runDirectoryTest.sh test-$name $@ SERVER=$KORE_RPC_BOOSTER ./runDirectoryTest.sh test-$name $@ ;; diff --git a/test/rpc-server/implies/implied-substitution/response.golden b/test/rpc-server/implies/implied-substitution/response.golden index 715a98ebbc..cf3900313b 100644 --- a/test/rpc-server/implies/implied-substitution/response.golden +++ b/test/rpc-server/implies/implied-substitution/response.golden @@ -1 +1 @@ -{"jsonrpc":"2.0","id":1,"result":{"valid":true,"implication":{"format":"KORE","version":1,"term":{"tag":"Implies","sort":{"tag":"SortApp","name":"SortK","args":[]},"first":{"tag":"EVar","name":"X","sort":{"tag":"SortApp","name":"SortK","args":[]}},"second":{"tag":"Exists","sort":{"tag":"SortApp","name":"SortK","args":[]},"var":"Z","varSort":{"tag":"SortApp","name":"SortK","args":[]},"arg":{"tag":"EVar","name":"Z","sort":{"tag":"SortApp","name":"SortK","args":[]}}}}},"condition":{"substitution":{"format":"KORE","version":1,"term":{"tag":"Equals","argSort":{"tag":"SortApp","name":"SortK","args":[]},"sort":{"tag":"SortApp","name":"SortK","args":[]},"first":{"tag":"EVar","name":"X","sort":{"tag":"SortApp","name":"SortK","args":[]}},"second":{"tag":"EVar","name":"Z","sort":{"tag":"SortApp","name":"SortK","args":[]}}}},"predicate":{"format":"KORE","version":1,"term":{"tag":"Top","sort":{"tag":"SortApp","name":"SortK","args":[]}}}}}} +{"jsonrpc":"2.0","id":1,"result":{"implication":{"format":"KORE","version":1,"term":{"tag":"Implies","sort":{"tag":"SortApp","name":"SortK","args":[]},"first":{"tag":"EVar","name":"X","sort":{"tag":"SortApp","name":"SortK","args":[]}},"second":{"tag":"Exists","sort":{"tag":"SortApp","name":"SortK","args":[]},"var":"Z","varSort":{"tag":"SortApp","name":"SortK","args":[]},"arg":{"tag":"EVar","name":"Z","sort":{"tag":"SortApp","name":"SortK","args":[]}}}}},"condition":{"substitution":{"format":"KORE","version":1,"term":{"tag":"Equals","argSort":{"tag":"SortApp","name":"SortK","args":[]},"sort":{"tag":"SortApp","name":"SortK","args":[]},"first":{"tag":"EVar","name":"X","sort":{"tag":"SortApp","name":"SortK","args":[]}},"second":{"tag":"EVar","name":"Z","sort":{"tag":"SortApp","name":"SortK","args":[]}}}},"predicate":{"format":"KORE","version":1,"term":{"tag":"Top","sort":{"tag":"SortApp","name":"SortK","args":[]}}}},"status":"valid"}} diff --git a/test/rpc-server/implies/implied-trivial/response.golden b/test/rpc-server/implies/implied-trivial/response.golden index 01a4878744..b308e0229e 100644 --- a/test/rpc-server/implies/implied-trivial/response.golden +++ b/test/rpc-server/implies/implied-trivial/response.golden @@ -1 +1 @@ -{"jsonrpc":"2.0","id":1,"result":{"valid":true,"implication":{"format":"KORE","version":1,"term":{"tag":"Implies","sort":{"tag":"SortVar","name":"S"},"first":{"tag":"EVar","name":"X","sort":{"tag":"SortVar","name":"S"}},"second":{"tag":"EVar","name":"X","sort":{"tag":"SortVar","name":"S"}}}},"condition":{"substitution":{"format":"KORE","version":1,"term":{"tag":"Top","sort":{"tag":"SortVar","name":"S"}}},"predicate":{"format":"KORE","version":1,"term":{"tag":"Top","sort":{"tag":"SortVar","name":"S"}}}}}} +{"jsonrpc":"2.0","id":1,"result":{"implication":{"format":"KORE","version":1,"term":{"tag":"Implies","sort":{"tag":"SortVar","name":"S"},"first":{"tag":"EVar","name":"X","sort":{"tag":"SortVar","name":"S"}},"second":{"tag":"EVar","name":"X","sort":{"tag":"SortVar","name":"S"}}}},"condition":{"substitution":{"format":"KORE","version":1,"term":{"tag":"Top","sort":{"tag":"SortVar","name":"S"}}},"predicate":{"format":"KORE","version":1,"term":{"tag":"Top","sort":{"tag":"SortVar","name":"S"}}}},"status":"valid"}} diff --git a/test/rpc-server/implies/not-implied-stuck/response.golden b/test/rpc-server/implies/not-implied-stuck/response.golden index dd21ebc198..f4c0797e69 100644 --- a/test/rpc-server/implies/not-implied-stuck/response.golden +++ b/test/rpc-server/implies/not-implied-stuck/response.golden @@ -1 +1 @@ -{"jsonrpc":"2.0","id":1,"result":{"valid":false,"implication":{"format":"KORE","version":1,"term":{"tag":"Implies","sort":{"tag":"SortApp","name":"SortK","args":[]},"first":{"tag":"EVar","name":"X","sort":{"tag":"SortApp","name":"SortK","args":[]}},"second":{"tag":"Exists","sort":{"tag":"SortApp","name":"SortK","args":[]},"var":"Z","varSort":{"tag":"SortApp","name":"SortK","args":[]},"arg":{"tag":"And","sort":{"tag":"SortApp","name":"SortK","args":[]},"patterns":[{"tag":"EVar","name":"Z","sort":{"tag":"SortApp","name":"SortK","args":[]}},{"tag":"Not","sort":{"tag":"SortApp","name":"SortK","args":[]},"arg":{"tag":"Equals","argSort":{"tag":"SortApp","name":"SortK","args":[]},"sort":{"tag":"SortApp","name":"SortK","args":[]},"first":{"tag":"EVar","name":"X","sort":{"tag":"SortApp","name":"SortK","args":[]}},"second":{"tag":"EVar","name":"Z","sort":{"tag":"SortApp","name":"SortK","args":[]}}}}]}}}},"condition":{"substitution":{"format":"KORE","version":1,"term":{"tag":"Equals","argSort":{"tag":"SortApp","name":"SortK","args":[]},"sort":{"tag":"SortApp","name":"SortK","args":[]},"first":{"tag":"EVar","name":"X","sort":{"tag":"SortApp","name":"SortK","args":[]}},"second":{"tag":"EVar","name":"Z","sort":{"tag":"SortApp","name":"SortK","args":[]}}}},"predicate":{"format":"KORE","version":1,"term":{"tag":"Top","sort":{"tag":"SortApp","name":"SortK","args":[]}}}}}} +{"jsonrpc":"2.0","id":1,"result":{"implication":{"format":"KORE","version":1,"term":{"tag":"Implies","sort":{"tag":"SortApp","name":"SortK","args":[]},"first":{"tag":"EVar","name":"X","sort":{"tag":"SortApp","name":"SortK","args":[]}},"second":{"tag":"Exists","sort":{"tag":"SortApp","name":"SortK","args":[]},"var":"Z","varSort":{"tag":"SortApp","name":"SortK","args":[]},"arg":{"tag":"And","sort":{"tag":"SortApp","name":"SortK","args":[]},"patterns":[{"tag":"EVar","name":"Z","sort":{"tag":"SortApp","name":"SortK","args":[]}},{"tag":"Not","sort":{"tag":"SortApp","name":"SortK","args":[]},"arg":{"tag":"Equals","argSort":{"tag":"SortApp","name":"SortK","args":[]},"sort":{"tag":"SortApp","name":"SortK","args":[]},"first":{"tag":"EVar","name":"X","sort":{"tag":"SortApp","name":"SortK","args":[]}},"second":{"tag":"EVar","name":"Z","sort":{"tag":"SortApp","name":"SortK","args":[]}}}}]}}}},"condition":{"substitution":{"format":"KORE","version":1,"term":{"tag":"Equals","argSort":{"tag":"SortApp","name":"SortK","args":[]},"sort":{"tag":"SortApp","name":"SortK","args":[]},"first":{"tag":"EVar","name":"X","sort":{"tag":"SortApp","name":"SortK","args":[]}},"second":{"tag":"EVar","name":"Z","sort":{"tag":"SortApp","name":"SortK","args":[]}}}},"predicate":{"format":"KORE","version":1,"term":{"tag":"Top","sort":{"tag":"SortApp","name":"SortK","args":[]}}}},"status":"invalid"}} diff --git a/test/rpc-server/implies/not-implied/response.golden b/test/rpc-server/implies/not-implied/response.golden index a1cf485402..7812c2eaa4 100644 --- a/test/rpc-server/implies/not-implied/response.golden +++ b/test/rpc-server/implies/not-implied/response.golden @@ -1 +1 @@ -{"jsonrpc":"2.0","id":1,"result":{"valid":false,"implication":{"format":"KORE","version":1,"term":{"tag":"Implies","sort":{"tag":"SortApp","name":"SortK","args":[]},"first":{"tag":"EVar","name":"X","sort":{"tag":"SortApp","name":"SortK","args":[]}},"second":{"tag":"Not","sort":{"tag":"SortApp","name":"SortK","args":[]},"arg":{"tag":"EVar","name":"X","sort":{"tag":"SortApp","name":"SortK","args":[]}}}}}}} +{"jsonrpc":"2.0","id":1,"result":{"implication":{"format":"KORE","version":1,"term":{"tag":"Implies","sort":{"tag":"SortApp","name":"SortK","args":[]},"first":{"tag":"EVar","name":"X","sort":{"tag":"SortApp","name":"SortK","args":[]}},"second":{"tag":"Not","sort":{"tag":"SortApp","name":"SortK","args":[]},"arg":{"tag":"EVar","name":"X","sort":{"tag":"SortApp","name":"SortK","args":[]}}}}},"status":"invalid"}}