ttuegel
commented
3 years ago Our first order of business should be to fix the error message.
Closed virgil-serbanuta closed 3 years ago
ttuegel
commented
3 years ago Our first order of business should be to fix the error message.
ttuegel
commented
3 years ago The error message was fixed in #2441.
MirceaS
commented
3 years ago @virgil-serbanuta Did you use the --bug-report option when generating that report?
If you did, then something seems to be going wrong, because the tar.gz was supposed to contain a script for reproducing what you're seeing.
If not, could you try using it and posting the results afterwards?
virgil-serbanuta
commented
3 years ago At the commit mentioned above I get:
$ /home/virgil/runtime-verification/kore/.build/kore/bin/kore-repl --smt-timeout 1000 --solver-transcript transcript.z3 vdefinition.kore --module EXECUTION --prove spec.kore --spec-module PROOF-UNSIGN --output result.kore --bug-report report
kore-repl --smt-timeout 1000 --solver-transcript transcript.z3 vdefinition.kore --module EXECUTION --prove spec.kore --spec-module PROOF-UNSIGN --output result.kore --bug-report report
KORE_REPL_OPTS=''
Invalid option `--bug-report'
[...]I used a newer version, so I'm not sure it's the same error as before:
Kore version 0.42.0.0
Git:
revision: 1b7a917c68da84187338f4c2ee29838b31d11fd8 (dirty)
branch: master
last commit: Thu Mar 25 15:49:32 2021 -0600and I run it with --bug-report, but I'm not sure that the archive contains what you want: report.tar.gz
/home/virgil/runtime-verification/kore/.build/kore/bin/kore-repl --smt-timeout 1000 --solver-transcript transcript.z3 vdefinition.kore --module EXECUTION --prove spec.kore --spec-module PROOF-UNSIGN --output result.kore --bug-report reportAnyway, here are the exact repl commands that I run:
step 13
select 13
step 4
select 19
step 22
select 41
step 14
select 56
step 14
select 71
step 10
select 82
step 31
select 114
step 100
exit@ttuegel I still get a badly printed error when I try to reporoduce this...
kore-repl: [649244697] Error (ErrorException):
WithConfiguration (Conditional {term = TermLike {getTermLike = Pattern {patternSort = SortActualSort (SortActual {sortActualName = Id {getId = "SortGeneratedTopCell", idLocation = AstLocationFile (FileLocation {fileName = "vdefinition.kore", line = 218, column = 83})}, sortActualSorts = []}), freeVariables = FreeVariables {getFreeVariables = fromList [(SomeVariableNameElement (ElementVariableName {unElementVariableName = VariableName {base = Id {getId = "Var'Unds'", idLocation = AstLocationFile (FileLocation {fileName = "vdefinition.kore", line = 4804, column = 78})}, counter = Just (Element 0)}}),SortActualSort (SortActual {sortActualName = Id {getId = "SortMap", idLocation = AstLocationFile (FileLocation {fileName = "vdefinition.kore", line = 4804, column = 89})}, sortActualSorts = []})),(SomeVariableNameElement (ElementVariableName {unElementVariableName = VariableName {base = Id {getId = "Var'Unds'", idLocation = AstLocationGeneratedVariable}, counter = Just (Element 1)}}),SortActualSort (SortActual {sortActualName = Id {getId = "SortInt", idLocation = AstLocationFile (FileLocation {fileName = "vdefinition.kore", line = 3642, column = 142})}, sortActualSorts = []})),(SomeVariableNameElement (ElementVariableName {unElementVariableName = VariableName {base = Id {getId = "Var'Unds'", idLocation = AstLocationGeneratedVariable}, counter = Just (Element 2)}}),SortActualSort (SortActual {sortActualName = Id {getId = "SortMap", idLocation = AstLocationFile (FileLocation {fileName = "vdefinition.kore", line = 4592, column = 80})}, sortActualSorts = []})),(SomeVariableNameElement (ElementVariableName {unElementVariableName = VariableName {base = Id {getId = "Var'Unds'", idLocation = AstLocationGeneratedVariable}, counter = Just (Element 3)}}),SortActualSort (SortActual {sortActualName = Id {getId = "SortMap", idLocation = AstLocationFile (FileLocation {fileName = "vdefinition.kore", line = 4538, column = 99})}, sortActualSorts = []})),(SomeVariableNameElement (ElementVariableName {unElementVariableName = VariableName {base = Id {getId = "Var'Unds'DotVar", idLocation = AstLocationGeneratedVariable}, counter = Just (Element 1)}}),SortActualSort (SortActual {sortActualName = Id {getId = "SortInt", idLocation = AstLocationFile (FileLocation {fileName = "vdefinition.kore", line = 3648, column = 132})}, sortActualSorts = []})),(SomeVariableNameElement (ElementVariableName {unElementVariableName = VariableName {base = Id {getId = "Var'Unds'DotVar", idLocation = AstLocationFile (FileLocation {fileName = "vdefinition.kore", line = 4606, column = 356})}, counter = Just (Element 7)}}),SortActualSort (SortActual {sortActualName = Id {getId = "SortMap", idLocation = AstLocationFile (FileLocation {fileName = "vdefinition.kore", line = 4606, column = 373})}, sortActualSorts = []})),(SomeVariableNameElement (ElementVariableName {unElementVariableName = VariableName {base = Id {getId = "VarAction", idLocation = AstLocationFile (FileLocation {fileName = "vdefinition.kore", line = 4808, column = 193})}, counter = Nothing}}),SortActualSort (SortActual {sortActualName = Id {getId = "SortKItem", idLocation = AstLocationFile (FileLocation {fileName = "vdefinition.kore", line = 4804, column = 27})}, sortActualSorts = []})),(SomeVariableNameElement (ElementVariableName {unElementVariableName = VariableName {base = Id {getId = "VarActionId", idLocation = AstLocationGeneratedVariable}, counter = Just (Element 0)}}),SortActualSort (SortActual {sortActualName = Id {getId = "SortInt", idLocation = AstLocationFile (FileLocation {fileName = "vdefinition.kore", line = 3675, column = 130})}, sortActualSorts = []})),(SomeVariableNameElement (ElementVariableName {unElementVariableName = VariableName {base = Id {getId = "VarActionLastIndex", idLocation = AstLocationGeneratedVariable}, counter = Just (Element 1)}}),SortActualSort (SortActual {sortActualName = Id {getId = "SortInt", idLocation = AstLocationFile (FileLocation {fileName = "vdefinition.kore", line = 3675, column = 130})}, sortActualSorts = []})),(SomeVariableNameElement (ElementVariableName {unElementVariableName = VariableName {base = Id {getId = "VarB", idLocation = AstLocationFile (FileLocation {fileName = "vdefinition.kore", line = 5912, column = 288})}, counter = Nothing}}),SortActualSort (SortActual {sortActualName = Id {getId = "SortInt", idLocation = AstLocationFile (FileLocation {fileName = "vdefinition.kore", line = 5910, column = 38})}, sortActualSorts = []})),(SomeVariableNameElement (ElementVariableName {unElementVariableName = VariableName {base = Id {getId = "VarEC", idLocation = AstLocationFile (FileLocation {fileName = "spec.kore", line = 14, column = 663})}, counter = Nothing}}),SortActualSort (SortActual {sortActualName = Id {getId = "SortExternalCommands", idLocation = AstLocationFile (FileLocation {fileName = "spec.kore", line = 14, column = 669})}, sortActualSorts = []})),(SomeVariableNameElement (ElementVariableName {unElementVariableName = VariableName {base = Id {getId = "VarI", idLocation = AstLocationFile (FileLocation {fileName = "vdefinition.kore", line = 4608, column = 164})}, counter = Nothing}}),SortActualSort (SortActual {sortActualName = Id {getId = "SortUsize", idLocation = AstLocationFile (FileLocation {fileName = "vdefinition.kore", line = 4606, column = 41})}, sortActualSorts = []})),(SomeVariableNameElement (ElementVariableName {unElementVariableName = VariableName {base = Id {getId = "VarNumBoardMembers", idLocation = AstLocationGeneratedVariable}, counter = Just (Element 0)}}),SortActualSort (SortActual {sortActualName = Id {getId = "SortInt", idLocation = AstLocationFile (FileLocation {fileName = "vdefinition.kore", line = 3675, column = 130})}, sortActualSorts = []})),(SomeVariableNameElement (ElementVariableName {unElementVariableName = VariableName {base = Id {getId = "VarNumProposers", idLocation = AstLocationGeneratedVariable}, counter = Just (Element 0)}}),SortActualSort (SortActual {sortActualName = Id {getId = "SortInt", idLocation = AstLocationFile (FileLocation {fileName = "vdefinition.kore", line = 3675, column = 130})}, sortActualSorts = []})),(SomeVariableNameElement (ElementVariableName {unElementVariableName = VariableName {base = Id {getId = "VarNumUsers", idLocation = AstLocationGeneratedVariable}, counter = Just (Element 0)}}),SortActualSort (SortActual {sortActualName = Id {getId = "SortInt", idLocation = AstLocationFile (FileLocation {fileName = "vdefinition.kore", line = 3675, column = 130})}, sortActualSorts = []})),(SomeVariableNameElement (ElementVariableName {unElementVariableName = VariableName {base = Id {getId = "VarQuorum", idLocation = AstLocationGeneratedVariable}, counter = Just (Element 0)}}),SortActualSort (SortActual {sortActualName = Id {getId = "SortInt", idLocation = AstLocationFile (FileLocation {fileName = "vdefinition.kore", line = 3675, column = 130})}, sortActualSorts = []})),(SomeVariableNameElement (ElementVariableName {unElementVariableName = VariableName {base = Id {getId = "VarSigners", idLocation = AstLocationFile (FileLocation {fileName = "vdefinition.kore", line = 4542, column = 169})}, counter = Nothing}}),SortActualSort (SortActual {sortActualName = Id {getId = "SortExpressionList", idLocation = AstLocationFile (FileLocation {fileName = "vdefinition.kore", line = 4542, column = 180})}, sortActualSorts = []})),(SomeVariableNameElement (ElementVariableName {unElementVariableName = VariableName {base = Id {getId = "VarUserIdToAddress", idLocation = AstLocationFile (FileLocation {fileName = "spec.kore", line = 14, column = 963})}, counter = Nothing}}),SortActualSort (SortActual {sortActualName = Id {getId = "SortMap", idLocation = AstLocationFile (FileLocation {fileName = "spec.kore", line = 14, column = 982})}, sortActualSorts = []}))]}, functional = Functional {isFunctional = False}, function = Function {isFunction = True}, defined = Defined {isDefined = False}, created = Created {getCreated = Nothing}, simplified = Simplified (SimplifiedData {sType = Fully, condition = Condition (Representation SideCondition VariableName _)}), constructorLike = ConstructorLike {getConstructorLike = Nothing}} :< ApplySymbolF (Application {applicationSymbolOrAlias = Symbol {symbolConstructor = Id {getId = "Lbl'-LT-'generatedTop'-GT-'", idLocation = AstLocationFile (FileLocation {fileName = "vdefinition.kore", line = 6298, column = 39})}, symbolParams = [], symbolSorts = ApplicationSorts {applicationSortsOperands = [SortActualSort (SortActual {sortActualName = Id {getId = "SortTCell", idLocation = AstLocationFile (FileLocation {fileName = "vdefinition.kore", line = 218, column = 40})}, sortActualSorts = []}),SortActualSort (SortActual {sortActualName = Id {getId = "SortGeneratedCounterCell", idLocation = AstLocationFile (FileLocation {fileName = "vdefinition.kore", line = 218, column = 53})}, sortActualSorts = []})], applicationSortsResult = SortActualSort (SortActual {sortActualName = Id {getId = "SortGeneratedTopCell", idLocation = AstLocationFile (FileLocation {fileName = "vdefinition.kore", line = 218, column = 83})}, sortActualSorts = []})}, symbolAttributes = Symbol {function = Function {isDeclaredFunction = False}, functional = Functional {isDeclaredFunctional = True}, constructor = Constructor {isConstructor = True}, injective = Injective {isDeclaredInjective = True}, sortInjection = SortInjection {isSortInjection = False}, anywhere = Anywhere {isAnywhere = False}, hook = Hook {getHook = Nothing}, smtlib = Smtlib {getSmtlib = Nothing}, smthook = Smthook {getSmthook = Nothing}, memo = Memo {isMemo = False}, klabel = Klabel {getKlabel = Nothing}, symbolKywd = SymbolKywd {isSymbolKywd = False}, noEvaluators = NoEvaluators {hasNoEvaluators = False}, sourceLocation = SourceLocation {location = Location {start = Nothing, end = Nothing}, source = Source {unSource = Nothing}}}}, applicationChildren = [TermLike {getTermLike = Pattern {patternSort = SortActualSort (SortActual {sortActualName = Id {getId = "SortTCell", idLocation = AstLocationFile (FileLocation {fileName = "vdefinition.kore", line = 218, column = 40})}, sortActualSorts = []}), freeVariables = FreeVariables {getFreeVariables = fromList [(SomeVariableNameElement (ElementVariableName {unElementVariableName = VariableName {base = Id {getId = "Var'Unds'", idLocation = AstLocationFile (FileLocation {fileName = "vdefinition.kore", line = 4804, column = 78})}, counter = Just (Element 0)}}),SortActualSort (SortActual {sortActualName = Id {getId = "SortMap", idLocation = AstLocationFile (FileLocation {fileName = "vdefinition.kore", line = 4804, column = 89})}, sortActualSorts = []})),(SomeVariableNameElement (ElementVariableName {unElementVariableName = VariableName {base = Id {getId = "Var'Unds'", idLocation = AstLocationGeneratedVariable}, counter = Just (Element 1)}}),SortActualSort (SortActual {sortActualName = Id {getId = "SortInt", idLocation = AstLocationFile (FileLocation {fileName = "vdefinition.kore", line = 3642, column = 142})}, sortActualSorts = []})),(SomeVariableNameElement (ElementVariableName {unElementVariableName = VariableName {base = Id {getId = "Var'Unds'", idLocation = AstLocationGeneratedVariable}, counter = Just (Element 2)}}),SortActualSort (SortActual {sortActualName = Id {getId = "SortMap", idLocation = AstLocationFile (FileLocation {fileName = "vdefinition.kore", line = 4592, column = 80})}, sortActualSorts = []})),(SomeVariableNameElement (ElementVariableName {unElementVariableName = VariableName {base = Id {getId = "Var'Unds'", idLocation = AstLocationGeneratedVariable}, counter = Just (Element 3)}}),SortActualSort (SortActual {sortActualName = Id {getId = "SortMap", idLocation = AstLocationFile (FileLocation {fileName = "vdefinition.kore", line = 4538, column = 99})}, sortActualSorts = []})),(SomeVariableNameElement (ElementVariableName {unElementVariableName = VariableName {base = Id {getId = "Var'Unds'DotVar", idLocation = AstLocationFile (FileLocation {fileName = "vdefinition.kore", line = 4606, column = 356})}, counter = Just (Element 7)}}),SortActualSort (SortActual {sortActualName = Id {getId = "SortMap", idLocation = AstLocationFile (FileLocation {fileName = "vdefinition.kore", line = 4606, column = 373})}, sortActualSorts = []})),(SomeVariableNameElement (ElementVariableName {unElementVariableName = VariableName {base = Id {getId = "VarAction", idLocation = AstLocationFile (FileLocation {fileName = "vdefinition.kore", line = 4808, column = 193})}, counter = Nothing}}),SortActualSort (SortActual {sortActualName = Id {getId = "SortKItem", idLocation = AstLocationFile (FileLocation {fileName = "vdefinition.kore", line = 4804, column = 27})}, sortActualSorts = []})),(SomeVariableNameElement (ElementVariableName {unElementVariableName = VariableName {base = Id {getId = "VarActionId", idLocation = AstLocationGeneratedVariable}, counter = Just (Element 0)}}),SortActualSort (SortActual {sortActualName = Id {getId = "SortInt", idLocation = AstLocationFile (FileLocation {fileName = "vdefinition.kore", line = 3675, column = 130})}, sortActualSorts = []})),(SomeVariableNameElement (ElementVariableName {unElementVariableName = VariableName {base = Id {getId = "VarActionLastIndex", idLocation = AstLocationGeneratedVariable}, counter = Just (Element 1)}}),SortActualSort (SortActual {sortActualName = Id {getId = "SortInt", idLocation = AstLocationFile (FileLocation {fileName = "vdefinition.kore", line = 3675, column = 130})}, sortActualSorts = []})),(SomeVariableNameElement (ElementVariableName {unElementVariableName = VariableName {base = Id {getId = "VarB", idLocation = AstLocationFile (FileLocation {fileName = "vdefinition.kore", line = 5912, column = 288})}, counter = Nothing}}),SortActualSort (SortActual {sortActualName = Id {getId = "SortInt", idLocation = AstLocationFile (FileLocation {fileName = "vdefinition.kore", line = 5910, column = 38})}, sortActualSorts = []})),(SomeVariableNameElement (ElementVariableName {unElementVariableName = VariableName {base = Id {getId = "VarEC", idLocation = AstLocationFile (FileLocation {fileName = "spec.kore", line = 14, column = 663})}, counter = Nothing}}),SortActualSort (SortActual {sortActualName = Id {getId = "SortExternalCommands", idLocation = AstLocationFile (FileLocation {fileName = "spec.kore", line = 14, column = 669})}, sortActualSorts = []})),(SomeVariableNameElement (ElementVariableName {unElementVariableName = VariableName {base = Id {getId = "VarI", idLocation = AstLocationFile (FileLocation {fileName = "vdefinition.kore", line = 4608, column = 164})}, counter = Nothing}}),SortActualSort (SortActual {sortActualName = Id {getId = "SortUsize", idLocation = AstLocationFile (FileLocation {fileName = "vdefinition.kore", line = 4606, column = 41})}, sortActualSorts = []})),(SomeVariableNameElement (ElementVariableName {unElementVariableName = VariableName {base = Id {getId = "VarNumBoardMembers", idLocation = AstLocationGeneratedVariable}, counter = Just (Element 0)}}),SortActualSort (SortActual {sortActualName = Id {getId = "SortInt", idLocation = AstLocationFile (FileLocation {fileName = "vdefinition.kore", line = 3675, column = 130})}, sortActualSorts = []})),(SomeVariableNameElement (ElementVariableName {unElementVariableName = VariableName {base = Id {getId = "VarNumProposers", idLocation = AstLocationGeneratedVariable}, counter = Just (Element 0)}}),SortActualSort (SortActual {sortActualName = Id {getId = "SortInt", idLocation = AstLocationFile (FileLocation {fileName = "vdefinition.kore", line = 3675, column = 130})}, sortActualSorts = []})),(SomeVariableNameElement (ElementVariableName {unElementVariableName = VariableName {base = Id {getId = "VarNumUsers", idLocation = AstLocationGeneratedVariable}, counter = Just (Element 0)}}),SortActualSort (SortActual {sortActualName = Id {getId = "SortInt", idLocation = AstLocationFile (FileLocation {fileName = "vdefinition.kore", line = 3675, column = 130})}, sortActualSorts = []})),(SomeVariableNameElement (ElementVariableName {unElementVariableName = VariableName {base = Id {getId = "VarQuorum", idLocation = AstLocationGeneratedVariable}, counter = Just (Element 0)}}),SortActualSort (SortActual {sortActualName = Id {getId = "SortInt", idLocation = AstLocationFile (FileLocation {fileName = "vdefinition.kore", line = 3675, column = 130})}, sortActualSorts = []})),(SomeVariableNameElement (ElementVariableName {unElementVariableName = VariableName {base = Id {getId = "VarSigners", idLocation = AstLocationFile (FileLocation {fileName = "vdefinition.kore", line = 4542, column = 169})}, counter = Nothing}}),SortActualSort (SortActual {sortActualName = Id {getId = "SortExpressionList", idLocation = AstLocationFile (FileLocation {fileName = "vdefinition.kore", line = 4542, column = 180})}, sortActualSorts = []})),(SomeVariableNameElement (ElementVariableName {unElementVariableName = VariableName {base = Id {getId = "VarUserIdToAddress", idLocation = AstLocationFile (FileLocation {fileName = "spec.kore", line = 14, column = 963})}, counter = Nothing}}),SortActualSort (SortActual {sortActualName = Id {getId = "SortMap", idLocation = AstLocationFile (FileLocation {fileName = "spec.kore", line = 14, column = 982})}, sortActualSorts = []}))]}, functional = Functional {isFunctional = False}, function = Function {isFunction = True}, defined = Defined {isDefined = False}, created = Created {getCreated = Nothing}, simplified = Simplified (SimplifiedData {sType = Fully, condition = Condition (Representation SideCondition VariableName _)}), constructorLike = ConstructorLike {getConstructorLike = Nothing}} :< ApplySymbolF (Application {applicationSymbolOrAlias = Symbol {symbolConstructor = Id {getId = "Lbl'-LT-'T'-GT-'", idLocation = AstLocationFile (FileLocation {fileName = "vdefinition.kore", line = 6298, column = 69})}, symbolParams = [], symbolSorts = ApplicationSorts {applicationSortsOperands = [SortActualSort (SortActual {sortActualName = Id {getId = "SortTTCell", idLocation = AstLocationFile (FileLocation {fileName = "vdefinition.kore", line = 200, column = 29})}, sortActualSorts = []})], applicationSortsResult = SortActualSort (SortActual {sortActualName = Id {getId = "SortTCell", idLocation = AstLocationFile (FileLocation {fileName = "vdefinition.kore", line = 200, column = 45})}, sortActualSorts = []})}, symbolAttributes = Symbol {function = Function {isDeclaredFunction = False}, functional = Functional {isDeclaredFunctional = True}, constructor = Constructor {isConstructor = True}, injective = Injective {isDeclaredInjective = True}, sortInjection = SortInjection {isSortInjection = False}, anywhere = Anywhere {isAnywhere = False}, hook = Hook {getHook = Nothing}, smtlib = Smtlib {getSmtlib = Nothing}, smthook = Smthook {getSmthook = Nothing}, memo = Memo {isMemo = False}, klabel = Klabel {getKlabel = Nothing}, symbolKywd = SymbolKywd {isSymbolKywd = False}, noEvaluators = NoEvaluators {hasNoEvaluators = False}, sourceLocation = SourceLocation {location = Location {start = Just (LineColumn {line = 924, column = 5}), end = Just (LineColumn {line = 958, column = 7})}, source = Source {unSource = Just "/home/virgil/runtime-verification/verified-smart-contracts/multisig/protocol-correctness/pseudocode.k"}}}}, applicationChildren = [TermLike {getTermLike = Pattern {patternSort = SortActualSort (SortActual {sortActualName = Id {getId = "SortTTCell", idLocation = AstLocationFile (FileLocation {fileName = "vdefinition.kore", line = 200, column = 29})}, sortActualSorts = []}), freeVariables = FreeVariables {getFreeVariables = fromList [(SomeVariableNameElement (ElementVariableName {unElementVariableName = VariableName {base = Id {getId = "Var'Unds'", idLocation = AstLocationFile (FileLocation {fileName = "vdefinition.kore", line = 4804, column = 78})}, counter = Just (Element 0)}}),SortActualSort (SortActual {sortActualName = Id {getId = "SortMap", idLocation = AstLocationFile (FileLocation {fileName = "vdefinition.kore", line = 4804, column = 89})}, sortActualSorts = []})),(SomeVariableNameElement (ElementVariableName {unElementVariableName = VariableName {base = Id {getId = "Var'Unds'", idLocation = AstLocationGeneratedVariable}, counter = Just (Element 1)}}),SortActualSort (SortActual {sortActualName = Id {getId = "SortInt", idLocation = AstLocationFile (FileLocation {fileName = "vdefinition.kore", line = 3642, column = 142})}, sortActualSorts = []})),(SomeVariableNameElement (ElementVariableName {unElementVariableName = VariableName {base = Id {getId = "Var'Unds'", idLocation = AstLocationGeneratedVariable}, counter = Just (Element 2)}}),SortActualSort (SortActual {sortActualName = Id {getId = "SortMap", idLocation = AstLocationFile (FileLocation {fileName = "vdefinition.kore", line = 4592, column = 80})}, sortActualSorts = []})),(SomeVariableNameElement (ElementVariableName {unElementVariableName = VariableName {base = Id {getId = "Var'Unds'", idLocation = AstLocationGeneratedVariable}, counter = Just (Element 3)}}),SortActualSort (SortActual {sortActualName = Id {getId = "SortMap", idLocation = AstLocationFile (FileLocation {fileName = "vdefinition.kore", line = 4538, column = 99})}, sortActualSorts = []})),(SomeVariableNameElement (ElementVariableName {unElementVariableName = VariableName {base = Id {getId = "Var'Unds'DotVar", idLocation = AstLocationFile (FileLocation {fileName = "vdefinition.kore", line = 4606, column = 356})}, counter = Just (Element 7)}}),SortActualSort (SortActual {sortActualName = Id {getId = "SortMap", idLocation = AstLocationFile (FileLocation {fileName = "vdefinition.kore", line = 4606, column = 373})}, sortActualSorts = []})),(SomeVariableNameElement (ElementVariableName {unElementVariableName = VariableName {base = Id {getId = "VarAction", idLocation = AstLocationFile (FileLocation {fileName = "vdefinition.kore", line = 4808, column = 193})}, counter = Nothing}}),SortActualSort (SortActual {sortActualName = Id {getId = "SortKItem", idLocation = AstLocationFile (FileLocation {fileName = "vdefinition.kore", line = 4804, column = 27})}, sortActualSorts = []})),(SomeVariableNameElement (ElementVariableName {unElementVariableName = VariableName {base = Id {getId = "VarActionId", idLocation = AstLocationGeneratedVariable}, counter = Just (Element 0)}}),SortActualSort (SortActual {sortActualName = Id {getId = "SortInt", idLocation = AstLocationFile (FileLocation {fileName = "vdefinition.kore", line = 3675, column = 130})}, sortActualSorts = []})),(SomeVariableNameElement (ElementVariableName {unElementVariableName = VariableName {base = Id {getId = "VarActionLastIndex", idLocation = AstLocationGeneratedVariable}, counter = Just (Element 1)}}),SortActualSort (SortActual {sortActualName = Id {getId = "SortInt", idLocation = AstLocationFile (FileLocation {fileName = "vdefinition.kore", line = 3675, column = 130})}, sortActualSorts = []})),(SomeVariableNameElement (ElementVariableName {unElementVariableName = VariableName {base = Id {getId = "VarB", idLocation = AstLocationFile (FileLocation {fileName = "vdefinition.kore", line = 5912, column = 288})}, counter = Nothing}}),SortActualSort (SortActual {sortActualName = Id {getId = "SortInt", idLocation = AstLocationFile (FileLocation {fileName = "vdefinition.kore", line = 5910, column = 38})}, sortActualSorts = []})),(SomeVariableNameElement (ElementVariableName {unElementVariableName = VariableName {base = Id {getId = "VarEC", idLocation = AstLocationFile (FileLocation {fileName = "spec.kore", line = 14, column = 663})}, counter = Nothing}}),SortActualSort (SortActual {sortActualName = Id {getId = "SortExternalCommands", idLocation = AstLocationFile (FileLocation {fileName = "spec.kore", line = 14, column = 669})}, sortActualSorts = []})),(SomeVariableNameElement (ElementVariableName {unElementVariableName = VariableName {base = Id {getId = "VarI", idLocation = AstLocationFile (FileLocation {fileName = "vdefinition.kore", line = 4608, column = 164})}, counter = Nothing}}),SortActualSort (SortActual {sortActualName = Id {getId = "SortUsize", idLocation = AstLocationFile (FileLocation {fileName = "vdefinition.kore", line = 4606, column = 41})}, sortActualSorts = []})),(SomeVariableNameElement (ElementVariableName {unElementVariableName = VariableName {base = Id {getId = "VarNumBoardMembers", idLocation = AstLocationGeneratedVariable}, counter = Just (Element 0)}}),SortActualSort (SortActual {sortActualName = Id {getId = "SortInt", idLocation = AstLocationFile (FileLocation {fileName = "vdefinition.kore", line = 3675, column = 130})}, sortActualSorts = []})),(SomeVariableNameElement (ElementVariableName {unElementVariableName = VariableName {base = Id {getId = "VarNumProposers", idLocation = AstLocationGeneratedVariable}, counter = Just (Element 0)}}),SortActualSort (SortActual {sortActualName = Id {getId = "SortInt", idLocation = AstLocationFile (FileLocation {fileName = "vdefinition.kore", line = 3675, column = 130})}, sortActualSorts = []})),(SomeVariableNameElement (ElementVariableName {unElementVariableName = VariableName {base = Id {getId = "VarNumUsers", idLocation = AstLocationGeneratedVariable}, counter = Just (Element 0)}}),SortActualSort (SortActual {sortActualName = Id {getId = "SortInt", idLocation = AstLocationFile (FileLocation {fileName = "vdefinition.kore", line = 3675, column = 130})}, sortActualSorts = []})),(SomeVariableNameElement (ElementVariableName {unElementVariableName = VariableName {base = Id {getId = "VarQuorum", idLocation = AstLocationGeneratedVariable}, counter = Just (Element 0)}}),SortActualSort (SortActual {sortActualName = Id {getId = "SortInt", idLocation = AstLocationFile (FileLocation {fileName = "vdefinition.kore", line = 3675, column = 130})}, sortActualSorts = []})),(SomeVariableNameElement (ElementVariableName {unElementVariableName = VariableName {base = Id {getId = "VarSigners", idLocation = AstLocationFile (FileLocation {fileName = "vdefinition.kore", line = 4542, column = 169})}, counter = Nothing}}),SortActualSort (SortActual {sortActualName = Id {getId = "SortExpressionList", idLocation = AstLocationFile (FileLocation {fileName = "vdefinition.kore", line = 4542, column = 180})}, sortActualSorts = []})),(SomeVariableNameElement (ElementVariableName {unElementVariableName = VariableName {base = Id {getId = "VarUserIdToAddress", idLocation = AstLocationFile (FileLocation {fileName = "spec.kore", line = 14, column = 963})}, counter = Nothing}}),SortActualSort (SortActual {sortActualName = Id {getId = "SortMap", idLocation = AstLocationFile (FileLocation {fileName = "spec.kore", line = 14, column = 982})}, sortActualSorts = []}))]}, functional = Functional {isFunctional = False}, function = Function {isFunction = True}, defined = Defined {isDefined = False}, created = Created {getCreated = Nothing}, simplified = Simplified (SimplifiedData {sType = Fully, condition = Condition (Representation SideCondition VariableName _)}), constructorLike = ConstructorLike {getConstructorLike = Nothing}} :< ApplySymbolF (Application {applicationSymbolOrAlias = Symbol {symbolConstructor = Id {getId = "Lbl'-LT-'TT'-GT-'", idLocation = AstLocationFile (FileLocation {fileName = "vdefinition.kore", line = 6298, column = 88})}, symbolParams = [], symbolSorts = ApplicationSorts {applicationSortsOperands = [SortActualSort (SortActual {sortActualName = Id {getId = "SortKCell", idLocation = AstLocationFile (FileLocation {fileName = "vdefinition.kore", line = 202, column = 30})}, sortActualSorts = []}),SortActualSort (SortActual {sortActualName = Id {getId = "SortStateCell", idLocation = AstLocationFile (FileLocation {fileName = "vdefinition.kore", line = 202, column = 43})}, sortActualSorts = []})], applicationSortsResult = SortActualSort (SortActual {sortActualName = Id {getId = "SortTTCell", idLocation = AstLocationFile (FileLocation {fileName = "vdefinition.kore", line = 202, column = 62})}, sortActualSorts = []})}, symbolAttributes = Symbol {function = Function {isDeclaredFunction = False}, functional = Functional {isDeclaredFunctional = True}, constructor = Constructor {isConstructor = True}, injective = Injective {isDeclaredInjective = True}, sortInjection = SortInjection {isSortInjection = False}, anywhere = Anywhere {isAnywhere = False}, hook = Hook {getHook = Nothing}, smtlib = Smtlib {getSmtlib = Nothing}, smthook = Smthook {getSmthook = Nothing}, memo = Memo {isMemo = False}, klabel = Klabel {getKlabel = Nothing}, symbolKywd = SymbolKywd {isSymbolKywd = False}, noEvaluators = NoEvaluators {hasNoEvaluators = False}, sourceLocation = SourceLocation {location = Location {start = Just (LineColumn {line = 924, column = 5}), end = Just (LineColumn {line = 958, column = 7})}, source = Source {unSource = Just "/home/virgil/runtime-verification/verified-smart-contracts/multisig/protocol-correctness/pseudocode.k"}}}}, applicationChildren = [TermLike {getTermLike = Pattern {patternSort = SortActualSort (SortActual {sortActualName = Id {getId = "SortKCell", idLocation = AstLocationFile (FileLocation {fileName = "vdefinition.kore", line = 202, column = 30})}, sortActualSorts = []}), freeVariables = FreeVariables {getFreeVariables = fromList [(SomeVariableNameElement (ElementVariableName {unElementVariableName = VariableName {base = Id {getId = "VarActionId", idLocation = AstLocationGeneratedVariable}, counter = Just (Element 0)}}),SortActualSort (SortActual {sortActualName = Id {getId = "SortInt", idLocation = AstLocationFile (FileLocation {fileName = "vdefinition.kore", line = 3675, column = 130})}, sortActualSorts = []})),(SomeVariableNameElement (ElementVariableName {unElementVariableName = VariableName {base = Id {getId = "VarB", idLocation = AstLocationFile (FileLocation {fileName = "vdefinition.kore", line = 5912, column = 288})}, counter = Nothing}}),SortActualSort (SortActual {sortActualName = Id {getId = "SortInt", idLocation = AstLocationFile (FileLocation {fileName = "vdefinition.kore", line = 5910, column = 38})}, sortActualSorts = []})),(SomeVariableNameElement (ElementVariableName {unElementVariableName = VariableName {base = Id {getId = "VarEC", idLocation = AstLocationFile (FileLocation {fileName = "spec.kore", line = 14, column = 663})}, counter = Nothing}}),SortActualSort (SortActual {sortActualName = Id {getId = "SortExternalCommands", idLocation = AstLocationFile (FileLocation {fileName = "spec.kore", line = 14, column = 669})}, sortActualSorts = []})),(SomeVariableNameElement (ElementVariableName {unElementVariableName = VariableName {base = Id {getId = "VarSigners", idLocation = AstLocationFile (FileLocation {fileName = "vdefinition.kore", line = 4542, column = 169})}, counter = Nothing}}),SortActualSort (SortActual {sortActualName = Id {getId = "SortExpressionList", idLocation = AstLocationFile (FileLocation {fileName = "vdefinition.kore", line = 4542, column = 180})}, sortActualSorts = []}))]}, functional = Functional {isFunctional = True}, function = Function {isFunction = True}, defined = Defined {isDefined = True}, created = Created {getCreated = Nothing}, simplified = Simplified (SimplifiedData {sType = Fully, condition = Condition (Representation SideCondition VariableName _)}), constructorLike = ConstructorLike {getConstructorLike = Nothing}} :< ApplySymbolF (Application {applicationSymbolOrAlias = Symbol {symbolConstructor = Id {getId = "Lbl'-LT-'k'-GT-'", idLocation = AstLocationFile (FileLocation {fileName = "vdefinition.kore", line = 6298, column = 108})}, symbolParams = [], symbolSorts = ApplicationSorts {applicationSortsOperands = [SortActualSort (SortActual {sortActualName = Id {getId = "SortK", idLocation = AstLocationFile (FileLocation {fileName = "vdefinition.kore", line = 220, column = 29})}, sortActualSorts = []})], applicationSortsResult = SortActualSort (SortActual {sortActualName = Id {getId = "SortKCell", idLocation = AstLocationFile (FileLocation {fileName = "vdefinition.kore", line = 220, column = 40})}, sortActualSorts = []})}, symbolAttributes = Symbol {function = Function {isDeclaredFunction = False}, functional = Functional {isDeclaredFunctional = True}, constructor = Constructor {isConstructor = True}, injective = Injective {isDeclaredInjective = True}, sortInjection = SortInjection {isSortInjection = False}, anywhere = Anywhere {isAnywhere = False}, hook = Hook {getHook = Nothing}, smtlib = Smtlib {getSmtlib = Nothing}, smthook = Smthook {getSmthook = Nothing}, memo = Memo {isMemo = False}, klabel = Klabel {getKlabel = Nothing}, symbolKywd = SymbolKywd {isSymbolKywd = False}, noEvaluators = NoEvaluators {hasNoEvaluators = False}, sourceLocation = SourceLocation {location = Location {start = Just (LineColumn {line = 924, column = 5}), end = Just (LineColumn {line = 958, column = 7})}, source = Source {unSource = Just "/home/virgil/runtime-verification/verified-smart-contracts/multisig/protocol-correctness/pseudocode.k"}}}}, applicationChildren = [TermLike {getTermLike = Pattern {patternSort = SortActualSort (SortActual {sortActualName = Id {getId = "SortK", idLocation = AstLocationFile (FileLocation {fileName = "vdefinition.kore", line = 220, column = 29})}, sortActualSorts = []}), freeVariables = FreeVariables {getFreeVariables = fromList [(SomeVariableNameElement (ElementVariableName {unElementVariableName = VariableName {base = Id {getId = "VarActionId", idLocation = AstLocationGeneratedVariable}, counter = Just (Element 0)}}),SortActualSort (SortActual {sortActualName = Id {getId = "SortInt", idLocation = AstLocationFile (FileLocation {fileName = "vdefinition.kore", line = 3675, column = 130})}, sortActualSorts = []})),(SomeVariableNameElement (ElementVariableName {unElementVariableName = VariableName {base = Id {getId = "VarB", idLocation = AstLocationFile (FileLocation {fileName = "vdefinition.kore", line = 5912, column = 288})}, counter = Nothing}}),SortActualSort (SortActual {sortActualName = Id {getId = "SortInt", idLocation = AstLocationFile (FileLocation {fileName = "vdefinition.kore", line = 5910, column = 38})}, sortActualSorts = []})),(SomeVariableNameElement (ElementVariableName {unElementVariableName = VariableName {base = Id {getId = "VarEC", idLocation = AstLocationFile (FileLocation {fileName = "spec.kore", line = 14, column = 663})}, counter = Nothing}}),SortActualSort (SortActual {sortActualName = Id {getId = "SortExternalCommands", idLocation = AstLocationFile (FileLocation {fileName = "spec.kore", line = 14, column = 669})}, sortActualSorts = []})),(SomeVariableNameElement (ElementVariableName {unElementVariableName = VariableName {base = Id {getId = "VarSigners", idLocation = AstLocationFile (FileLocation {fileName = "vdefinition.kore", line = 4542, column = 169})}, counter = Nothing}}),SortActualSort (SortActual {sortActualName = Id {getId = "SortExpressionList", idLocation = AstLocationFile (FileLocation {fileName = "vdefinition.kore", line = 4542, column = 180})}, sortActualSorts = []}))]}, functional = Functional {isFunctional = True}, function = Function {isFunction = True}, defined = Defined {isDefined = True}, created = Created {getCreated = Nothing}, simplified = Simplified (SimplifiedData {sType = Fully, condition = Condition (Representation SideCondition VariableName _)}), constructorLike = ConstructorLike {getConstructorLike = Nothing}} :< ApplySymbolF (Application {applicationSymbolOrAlias = Symbol {symbolConstructor = Id {getId = "kseq", idLocation = AstLocationFile (FileLocation {fileName = "vdefinition.kore", line = 5404, column = 190})}, symbolParams = [], symbolSorts = ApplicationSorts {applicationSortsOperands = [SortActualSort (SortActual {sortActualName = Id {getId = "SortKItem", idLocation = AstLocationFile (FileLocation {fileName = "vdefinition.kore", line = 12, column = 17})}, sortActualSorts = []}),SortActualSort (SortActual {sortActualName = Id {getId = "SortK", idLocation = AstLocationFile (FileLocation {fileName = "vdefinition.kore", line = 12, column = 30})}, sortActualSorts = []})], applicationSortsResult = SortActualSort (SortActual {sortActualName = Id {getId = "SortK", idLocation = AstLocationFile (FileLocation {fileName = "vdefinition.kore", line = 12, column = 41})}, sortActualSorts = []})}, symbolAttributes = Symbol {function = Function {isDeclaredFunction 
ana-pantilie
commented
3 years ago @MirceaS , in case you didn't already know, you can add the repl commands to a file and run the spec with --repl-script <file> to run all those steps automatically.
MirceaS
commented
3 years ago Error as it is printed now:
kore-repl: [112384137] Error (ErrorDecidePredicateUnknown):
Failed to decide predicate:
/* Sfa */
\not{_PREDICATE{}}(
/* Sfa */
\equals{SortBool{}, _PREDICATE{}}(
/* Fl Fn D Sfa Cl */ \dv{SortBool{}}("true"),
/* Fl Fn D Sfa */
Lbl'Unds-GT-'Int'Unds'{}(
/* Fl Fn D Sfa */
Lbl'UndsPlus'Int'Unds'{}(
/* Fl Fn D Sfa */ VarActionLastIndex1:SortInt{},
/* Fl Fn D Sfa Cl */ \dv{SortInt{}}("2")
),
/* Fl Fn D Sfa */ VarActionId0:SortInt{}
)
)
)
with side condition:
/* Spu */
\and{_PREDICATE{}}(
/* Sfc */
\equals{SortUsize{}, _PREDICATE{}}(
/* Fl Fn D Sfc */
Lbl'Hash'listFind'LParUndsCommUndsRParUnds'PSEUDOCODE-FUNCTIONS'Unds'Usize'Unds'ExpressionList'Unds'Expression{}(
/* Fl Fn D Sfa */ VarSigners:SortExpressionList{},
/* Fl Fn D Sfc */
/* Inj: */ inj{SortUsize{}, SortExpression{}}(
/* Fl Fn D Sfa */ VarI:SortUsize{}
)
),
/* Fl Fn D Sfa */
Lblu'LParUndsRParUnds'PSEUDOCODE-SYNTAX'Unds'Usize'Unds'Int{}(
/* Fl Fn D Sfa */ VarB:SortInt{}
)
),
/* Spu */
\and{_PREDICATE{}}(
/* Sfc */
\equals{SortBool{}, _PREDICATE{}}(
/* Fl Fn D Sfa Cl */ \dv{SortBool{}}("false"),
/* Fl Fn D Sfc */
Lbl'Unds'in'Unds'keys'LParUndsRParUnds'MAP'Unds'Bool'Unds'KItem'Unds'Map{}(
/* Fl Fn D Sfc */
/* Inj: */ inj{SortAddress{}, SortKItem{}}(
/* Fl Fn D Sfa */
Lbladdress'LParUndsRParUnds'PSEUDOCODE-SYNTAX'Unds'Address'Unds'Int{}(
/* Fl Fn D Sfa */ Var'Unds'1:SortInt{}
)
),
/* Fl Fn D Sfa */ Var'Unds'DotVar7:SortMap{}
)
),
/* Spu */
\and{_PREDICATE{}}(
/* Sfc */
\equals{SortBool{}, _PREDICATE{}}(
/* Fl Fn D Sfa Cl */ \dv{SortBool{}}("false"),
/* Fl Fn D Sfc */
Lbl'Unds'in'Unds'keys'LParUndsRParUnds'MAP'Unds'Bool'Unds'KItem'Unds'Map{}(
/* Fl Fn D Sfc */
/* Inj: */ inj{SortUsize{}, SortKItem{}}(
/* Fl Fn D Sfa */
Lblu'LParUndsRParUnds'PSEUDOCODE-SYNTAX'Unds'Usize'Unds'Int{}(
/* Fl Fn D Sfa */
Lbl'UndsPlus'Int'Unds'{}(
/* Fl Fn D Sfa */
VarActionLastIndex1:SortInt{},
/* Fl Fn D Sfa Cl */ \dv{SortInt{}}("1")
)
)
),
/* Fl Fn D Sfa */ Var'Unds'0:SortMap{}
)
),
/* Spu */
\and{_PREDICATE{}}(
/* Sfc */
\equals{SortBool{}, _PREDICATE{}}(
/* Fl Fn D Sfa Cl */ \dv{SortBool{}}("false"),
/* Fl Fn D Sfc */
Lbl'Unds'in'Unds'keys'LParUndsRParUnds'MAP'Unds'Bool'Unds'KItem'Unds'Map{}(
/* Fl Fn D Sfc */
/* Inj: */ inj{SortUsize{}, SortKItem{}}(
/* Fl Fn D Sfa */
Lblu'LParUndsRParUnds'PSEUDOCODE-SYNTAX'Unds'Usize'Unds'Int{}(
/* Fl Fn D Sfa */
Lbl'UndsPlus'Int'Unds'{}(
/* Fl Fn D Sfa */
VarActionLastIndex1:SortInt{},
/* Fl Fn D Sfa Cl */
\dv{SortInt{}}("1")
)
)
),
/* Created: Kore.Step.RewriteStep.resetResultPattern */
/* Fl Fn D Sfa */
Var'Unds'3:SortMap{}
)
),
/* Spu */
\and{_PREDICATE{}}(
/* Sfa */
\equals{SortBool{}, _PREDICATE{}}(
/* Fl Fn D Sfa Cl */ \dv{SortBool{}}("false"),
/* Fl Fn D Sfa */
Lbl'Unds'in'Unds'keys'LParUndsRParUnds'MAP'Unds'Bool'Unds'KItem'Unds'Map{}(
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortUsize{}, SortKItem{}}(
/* Fl Fn D Sfa Cl */
Lblu'LParUndsRParUnds'PSEUDOCODE-SYNTAX'Unds'Usize'Unds'Int{}(
/* Fl Fn D Sfa Cl */
\dv{SortInt{}}("0")
)
),
/* Created: Kore.Step.RewriteStep.resetResultPattern */
/* Fl Fn D Sfa */
Var'Unds'2:SortMap{}
)
),
/* Spu */
\and{_PREDICATE{}}(
/* Sfa */
\equals{SortBool{}, _PREDICATE{}}(
/* Fl Fn D Sfa Cl */
\dv{SortBool{}}("false"),
/* Fl Fn D Sfa */
Lbl'Unds'in'Unds'keys'LParUndsRParUnds'MAP'Unds'Bool'Unds'KItem'Unds'Map{}(
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortUsize{}, SortKItem{}}(
/* Fl Fn D Sfa Cl */
Lblu'LParUndsRParUnds'PSEUDOCODE-SYNTAX'Unds'Usize'Unds'Int{}(
/* Fl Fn D Sfa Cl */
\dv{SortInt{}}("0")
)
),
/* Fl Fn D Sfa */
VarUserIdToAddress:SortMap{}
)
),
/* Spu */
\and{_PREDICATE{}}(
/* Sfc */
\equals{SortBool{}, _PREDICATE{}}(
/* Fl Fn D Sfa Cl */
\dv{SortBool{}}("false"),
/* Fl Fn D Sfc */
Lbl'Unds'in'Unds'keys'LParUndsRParUnds'MAP'Unds'Bool'Unds'KItem'Unds'Map{}(
/* Fl Fn D Sfc */
/* Inj: */ inj{SortUsize{}, SortKItem{}}(
/* Fl Fn D Sfa */
Lblu'LParUndsRParUnds'PSEUDOCODE-SYNTAX'Unds'Usize'Unds'Int{}(
/* Fl Fn D Sfa */
VarActionId0:SortInt{}
)
),
/* Fl Fn D Sfa */
Var'Unds'0:SortMap{}
)
),
/* Spu */
\and{_PREDICATE{}}(
/* Sfc */
\equals{SortBool{}, _PREDICATE{}}(
/* Fl Fn D Sfa Cl */
\dv{SortBool{}}("false"),
/* Fl Fn D Sfc */
Lbl'Unds'in'Unds'keys'LParUndsRParUnds'MAP'Unds'Bool'Unds'KItem'Unds'Map{}(
/* Fl Fn D Sfc */
/* Inj: */ inj{SortUsize{}, SortKItem{}}(
/* Fl Fn D Sfa */
Lblu'LParUndsRParUnds'PSEUDOCODE-SYNTAX'Unds'Usize'Unds'Int{}(
/* Fl Fn D Sfa */
VarActionId0:SortInt{}
)
),
/* Created: Kore.Step.RewriteStep.resetResultPattern */
/* Fl Fn D Sfa */
Var'Unds'3:SortMap{}
)
),
/* Spu */
\and{_PREDICATE{}}(
/* Sfc */
\equals{SortBool{}, _PREDICATE{}}(
/* Fl Fn D Sfa Cl */
\dv{SortBool{}}("false"),
/* Fl Fn D Sfc */
Lbl'Unds'in'Unds'keys'LParUndsRParUnds'MAP'Unds'Bool'Unds'KItem'Unds'Map{}(
/* Fl Fn D Sfc */
/* Inj: */ inj{SortUsize{}, SortKItem{}}(
/* Fl Fn D Sfa */
VarI:SortUsize{}
),
/* Created: Kore.Step.RewriteStep.resetResultPattern */
/* Fl Fn D Sfa */
Var'Unds'2:SortMap{}
)
),
/* Spu */
\and{_PREDICATE{}}(
/* Sfc */
\equals{SortBool{}, _PREDICATE{}}(
/* Fl Fn D Sfa Cl */
\dv{SortBool{}}("true"),
/* Fn Sfc */
Lbl'Hash'unusedActionIds'LParUndsCommUndsCommUndsRParUnds'INVARIANT'Unds'Bool'Unds'Usize'Unds'Map'Unds'Int{}(
/* Fl Fn D Sfa */
Lblu'LParUndsRParUnds'PSEUDOCODE-SYNTAX'Unds'Usize'Unds'Int{}(
/* Fl Fn D Sfa */
Lbl'UndsPlus'Int'Unds'{}(
/* Fl Fn D Sfa */
VarActionLastIndex1:SortInt{},
/* Fl Fn D Sfa Cl */
\dv{SortInt{}}("2")
)
),
/* Fn Sfc */
/* InternalMap: */ Lbl'Unds'Map'Unds'{}(
/* element: */ Lbl'UndsPipe'-'-GT-Unds'{}(
/* Fl Fn D Sfc */
/* Inj: */ inj{SortUsize{}, SortKItem{}}(
/* Fl Fn D Sfa */
Lblu'LParUndsRParUnds'PSEUDOCODE-SYNTAX'Unds'Usize'Unds'Int{}(
/* Fl Fn D Sfa */
VarActionId0:SortInt{}
)
),
/* Fl Fn D Sfc */
/* Inj: */ inj{SortExpressionList{}, SortKItem{}}(
/* Fl Fn D Sfa */
VarSigners:SortExpressionList{}
)
),
/* opaque child: */ /* Created: Kore.Step.RewriteStep.resetResultPattern */
/* Fl Fn D Sfa */
Var'Unds'3:SortMap{}
),
/* Fl Fn D Sfa Cl */
\dv{SortInt{}}("0")
)
),
/* Spu */
\and{_PREDICATE{}}(
/* Sfc */
\equals{SortBool{}, _PREDICATE{}}(
/* Fl Fn D Sfa Cl */
\dv{SortBool{}}("true"),
/* Fl Fn D Sfc */
Lbl'Unds'in'Unds'keys'LParUndsRParUnds'MAP'Unds'Bool'Unds'KItem'Unds'Map{}(
/* Fl Fn D Sfc */
/* Inj: */ inj{SortUsize{}, SortKItem{}}(
/* Fl Fn D Sfa */
VarI:SortUsize{}
),
/* Fl Fn D Sfa */
VarUserIdToAddress:SortMap{}
)
),
/* Spu */
\and{_PREDICATE{}}(
/* Sfa */
\equals{SortBool{}, _PREDICATE{}}(
/* Fl Fn D Sfa Cl */
\dv{SortBool{}}("true"),
/* Fl Fn D Sfa */
Lbl'Unds-LT-Eqls'Int'Unds'{}(
/* Fl Fn D Sfa Cl */
\dv{SortInt{}}("0"),
/* Fl Fn D Sfa */
VarB:SortInt{}
)
),
/* Spu */
\and{_PREDICATE{}}(
/* Sfc */
\equals{SortBool{}, _PREDICATE{}}(
/* Fl Fn D Sfa Cl */
\dv{SortBool{}}("true"),
/* Fn Sfc */
LblallValuesBecomeKeys'LParUndsCommUndsRParUnds'INVARIANT'Unds'Bool'Unds'Map'Unds'Map{}(
/* Fl Fn D Sfa */
Var'Unds'DotVar7:SortMap{},
/* Fn Sfc */
/* InternalMap: */ Lbl'Unds'Map'Unds'{}(
/* element: */ Lbl'UndsPipe'-'-GT-Unds'{}(
/* Fl Fn D Sfc */
/* Inj: */ inj{SortUsize{}, SortKItem{}}(
/* Fl Fn D Sfa */
VarI:SortUsize{}
),
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortUserRole{}, SortKItem{}}(
/* Fl Fn D Sfa Cl */
LblBoardMember'Unds'PSEUDOCODE-SYNTAX'Unds'UserRole{}()
)
),
/* opaque child: */ /* Created: Kore.Step.RewriteStep.resetResultPattern */
/* Fl Fn D Sfa */
Var'Unds'2:SortMap{}
)
)
),
/* Spu */
\and{_PREDICATE{}}(
/* Sfa */
\equals{SortBool{}, _PREDICATE{}}(
/* Fl Fn D Sfa Cl */
\dv{SortBool{}}("true"),
/* Fl Fn D Sfa */
LblallValuesBecomeKeys'LParUndsCommUndsRParUnds'INVARIANT'Unds'Bool'Unds'Map'Unds'Map{}(
/* Fl Fn D Sfa */
Var'Unds'DotVar7:SortMap{},
/* Fl Fn D Sfa */
VarUserIdToAddress:SortMap{}
)
),
/* Spu */
\and{_PREDICATE{}}(
/* Sfc */
\equals{SortBool{}, _PREDICATE{}}(
/* Fl Fn D Sfa Cl */
\dv{SortBool{}}("true"),
/* Fn Sfc */
LblisKResult{}(
/* Fl Fn D Sfc */
kseq{}(
/* Fl Fn D Sfc */
/* Inj: */ inj{SortExpressionList{}, SortKItem{}}(
/* Fl Fn D Sfa */
VarSigners:SortExpressionList{}
),
/* Fl Fn D Sfa Cl */
dotk{}()
)
)
),
/* Spu */
\and{_PREDICATE{}}(
/* Sfc */
\equals{SortBool{}, _PREDICATE{}}(
/* Fl Fn D Sfa Cl */
\dv{SortBool{}}("true"),
/* Fn Sfc */
LblkeysSubset'LParUndsCommUndsRParUnds'INVARIANT'Unds'Bool'Unds'Map'Unds'Map{}(
/* Fl Fn D Sfa */
Var'Unds'0:SortMap{},
/* Fn Sfc */
/* InternalMap: */ Lbl'Unds'Map'Unds'{}(
/* element: */ Lbl'UndsPipe'-'-GT-Unds'{}(
/* Fl Fn D Sfc */
/* Inj: */ inj{SortUsize{}, SortKItem{}}(
/* Fl Fn D Sfa */
Lblu'LParUndsRParUnds'PSEUDOCODE-SYNTAX'Unds'Usize'Unds'Int{}(
/* Fl Fn D Sfa */
VarActionId0:SortInt{}
)
),
/* Fl Fn D Sfc */
/* Inj: */ inj{SortExpressionList{}, SortKItem{}}(
/* Fl Fn D Sfa */
VarSigners:SortExpressionList{}
)
),
/* opaque child: */ /* Created: Kore.Step.RewriteStep.resetResultPattern */
/* Fl Fn D Sfa */
Var'Unds'3:SortMap{}
)
)
),
/* Spc */
\and{_PREDICATE{}}(
/* Sfc */
\equals{SortBool{}, _PREDICATE{}}(
/* Fl Fn D Sfa Cl */
\dv{SortBool{}}("true"),
/* Fn Sfc */
LblkeysSubset'LParUndsCommUndsRParUnds'INVARIANT'Unds'Bool'Unds'Map'Unds'Map{}(
/* Created: Kore.Step.RewriteStep.resetResultPattern */
/* Fl Fn D Sfa */
Var'Unds'3:SortMap{},
/* Fn Sfc */
/* InternalMap: */ Lbl'Unds'Map'Unds'{}(
/* element: */ Lbl'UndsPipe'-'-GT-Unds'{}(
/* Fl Fn D Sfc */
/* Inj: */ inj{SortUsize{}, SortKItem{}}(
/* Fl Fn D Sfa */
Lblu'LParUndsRParUnds'PSEUDOCODE-SYNTAX'Unds'Usize'Unds'Int{}(
/* Fl Fn D Sfa */
VarActionId0:SortInt{}
)
),
/* Fl Fn D Sfa */
VarAction:SortKItem{}
),
/* opaque child: */ /* Fl Fn D Sfa */
Var'Unds'0:SortMap{}
)
)
),
/* Spa */
\and{_PREDICATE{}}(
/* Sfa */
\equals{SortBool{}, _PREDICATE{}}(
/* Fl Fn D Sfa Cl */
\dv{SortBool{}}("true"),
/* Fl Fn D Sfa */
LblvaluesAreExpressionList'LParUndsRParUnds'INVARIANT'Unds'Bool'Unds'Map{}(
/* Created: Kore.Step.RewriteStep.resetResultPattern */
/* Fl Fn D Sfa */
Var'Unds'3:SortMap{}
)
),
/* Spa */
\and{_PREDICATE{}}(
/* Sfa */
\equals{SortBool{}, _PREDICATE{}}(
/* Fl Fn D Sfa Cl */
\dv{SortBool{}}("true"),
/* Fl Fn D Sfa */
LblvaluesAreKResult'LParUndsRParUnds'INVARIANT'Unds'Bool'Unds'Map{}(
/* Created: Kore.Step.RewriteStep.resetResultPattern */
/* Fl Fn D Sfa */
Var'Unds'3:SortMap{}
)
),
/* Spa */
\and{_PREDICATE{}}(
/* Sfa */
\not{_PREDICATE{}}(
/* Spa */
\and{_PREDICATE{}}(
/* Sfa */
\exists{_PREDICATE{}}(
Var'Unds'0:SortExpression{},
/* Sfa */
\exists{_PREDICATE{}}(
VarL:SortExpressionCSV{},
/* Spa */
\equals{SortExpressionList{}, _PREDICATE{}}(
/* Fl Fn D Sfa */
VarSigners:SortExpressionList{},
/* Fl Fn D Sfa */
Lbl'LSqBUndsRSqBUnds'PSEUDOCODE-SYNTAX'Unds'ExpressionList'Unds'ExpressionCSV{}(
/* Fl Fn D Sfa */
Lbl'UndsCommUndsUnds'PSEUDOCODE-SYNTAX'Unds'ExpressionCSV'Unds'Expression'Unds'ExpressionCSV{}(
/* Fl Fn D Sfa */
Var'Unds'0:SortExpression{},
/* Fl Fn D Sfa */
VarL:SortExpressionCSV{}
)
)
)
)
),
/* Spa */
\equals{SortInt{}, _PREDICATE{}}(
/* Fl Fn D Sfa */
VarB:SortInt{},
/* Fl Fn D Sfa Cl */
\dv{SortInt{}}("0")
)
)
),
/* Spa */
\and{_PREDICATE{}}(
/* Sfa */
\not{_PREDICATE{}}(
/* Spa */
\equals{SortKItem{}, _PREDICATE{}}(
/* Fl Fn D Sfa */
VarAction:SortKItem{},
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortAction{}, SortKItem{}}(
/* Fl Fn D Sfa Cl */
LblNothing'Unds'PSEUDOCODE-SYNTAX'Unds'Action{}()
)
)
),
/* Spa */
\and{_PREDICATE{}}(
/* Sfa */
\not{_PREDICATE{}}(
/* Spa */
\equals{SortInt{}, _PREDICATE{}}(
/* Fl Fn D Sfa */
VarActionId0:SortInt{},
/* Fl Fn D Sfa */
Lbl'UndsPlus'Int'Unds'{}(
/* Fl Fn D Sfa */
VarActionLastIndex1:SortInt{},
/* Fl Fn D Sfa Cl */
\dv{SortInt{}}("1")
)
)
),
/* Spa */
\and{_PREDICATE{}}(
/* Sfa */
\not{_PREDICATE{}}(
/* Spa */
\equals{SortUsize{}, _PREDICATE{}}(
/* Fl Fn D Sfa */
VarI:SortUsize{},
/* Fl Fn D Sfa Cl */
Lblu'LParUndsRParUnds'PSEUDOCODE-SYNTAX'Unds'Usize'Unds'Int{}(
/* Fl Fn D Sfa Cl */
\dv{SortInt{}}("0")
)
)
),
/* Sfa */
\not{_PREDICATE{}}(
/* Sfa */
\exists{_PREDICATE{}}(
VarE:SortExpression{},
/* Sfa */
\exists{_PREDICATE{}}(
VarL:SortExpressionCSV{},
/* Spa */
\and{_PREDICATE{}}(
/* Sfa */
\equals{SortBool{}, _PREDICATE{}}(
/* Fl Fn D Sfa Cl */
\dv{SortBool{}}("true"),
/* Fl Fn D Sfa */
Lbl'Unds-GT-'Int'Unds'{}(
/* Fl Fn D Sfa */
VarB:SortInt{},
/* Fl Fn D Sfa Cl */
\dv{SortInt{}}("0")
)
),
/* Spa */
\equals{SortExpressionList{}, _PREDICATE{}}(
/* Fl Fn D Sfa */
VarSigners:SortExpressionList{},
/* Fl Fn D Sfa */
Lbl'LSqBUndsRSqBUnds'PSEUDOCODE-SYNTAX'Unds'ExpressionList'Unds'ExpressionCSV{}(
/* Fl Fn D Sfa */
Lbl'UndsCommUndsUnds'PSEUDOCODE-SYNTAX'Unds'ExpressionCSV'Unds'Expression'Unds'ExpressionCSV{}(
/* Fl Fn D Sfa */
VarE:SortExpression{},
/* Fl Fn D Sfa */
VarL:SortExpressionCSV{}
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)@virgil-serbanuta We think that the above is too complex for the SMT solver to solve. Is this something you can work with/around now?
virgil-serbanuta
commented
3 years ago I think I can work around that.
MirceaS
commented
3 years ago @virgil-serbanuta Cool! I'll close this issue then. The latest master has the error messaging fix.
To reproduce:
Use this Kore version:
In the repl I use the following:
The last line should probably be something like
step 13orstep 14to go just before the error, and one more step to produce it.dot.kprove-2021-01-26-18-38-39-058-488069ab-7975-4c27-b29c-b0d471c2a8b8.zip
kore-repl.tar.gz