API tools faq
paste
Guest User

Untitled

a guest
Jan 7th, 2021
245
0
Never
Add comment
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
Python 98.69 KB | None | 0 0
raw download clone embed print report
  1. import logging
  2. from multiprocessing import Pool, log_to_stderr
  3. import json
  4.  
  5. DATA = json.loads('''
  6. [["set-option", ":print-success", "false"], ["set-info", ":smt-lib-version", "2.0"], ["set-option", ":produce-models", "true"], ["set-option", ":AUTO_CONFIG", "false"], ["set-option", ":pp.bv_literals", "false"], ["set-option", ":MODEL.V2", "true"], ["set-option", ":smt.PHASE_SELECTION", "0"], ["set-option", ":smt.RESTART_STRATEGY", "0"], ["set-option", ":smt.RESTART_FACTOR", "|1.5|"], ["set-option", ":smt.ARITH.RANDOM_INITIAL_VALUE", "true"], ["set-option", ":smt.CASE_SPLIT", "3"], ["set-option", ":smt.DELAY_UNITS", "true"], ["set-option", ":NNF.SK_HACK", "true"], ["set-option", ":smt.MBQI", "false"], ["set-option", ":smt.QI.EAGER_THRESHOLD", "100"], ["set-option", ":TYPE_CHECK", "true"], ["set-option", ":smt.BV.REFLECT", "true"], ["set-option", ":model_compress", "false"], "; done setting options", ["declare-fun", "tickleBool", ["Bool"], "Bool"], ["assert", ["and", ["tickleBool", "true"], ["tickleBool", "false"]]], ["declare-sort", "T@FieldName", "0"], ["declare-sort", "T@String", "0"], ["declare-datatypes", [["T@Edge", "0"]], [[["Field", ["|f#Field|", "T@FieldName"]], ["Index", ["|i#Index|", "Int"]], ["String", ["|s#String|", "T@String"]]]]], ["declare-sort", "T@Address", "0"], ["declare-datatypes", [["T@Value", "0"]], [[["Boolean", ["|b#Boolean|", "Bool"]], ["Integer", ["|i#Integer|", "Int"]], ["Address", ["|a#Address|", "T@Address"]], ["Map", ["|m#Map|", ["Array", "T@Edge", "T@Value"]]]]]], ["declare-datatypes", [["T@ResourceStore", "0"]], [[["ResourceStore", ["|domain#ResourceStore|", ["Array", "T@Address", "Bool"]], ["|contents#ResourceStore|", ["Array", "T@Address", "T@Value"]]]]]], ["declare-datatypes", [["T@Path", "0"]], [[["Nil"], ["Cons", ["|p#Cons|", "T@Path"], ["|e#Cons|", "T@Edge"]]]]], ["declare-sort", "T@TypeName", "0"], ["declare-sort", "T@LocalName", "0"], ["declare-datatypes", [["T@Reference", "0"]], [[["GlobalReference", ["|a#GlobalReference|", "T@Address"], ["|t#GlobalReference|", "T@TypeName"], ["|p#GlobalReference|", "T@Path"], ["|v#GlobalReference|", "T@Value"]], ["LocalReference", ["|c#LocalReference|", "Int"], ["|l#LocalReference|", "T@LocalName"], ["|p#LocalReference|", "T@Path"], ["|v#LocalReference|", "T@Value"]]]]], ["declare-fun", "TestReference_T", [], "T@TypeName"], ["declare-fun", "TestReference_T_value", [], "T@FieldName"], ["declare-fun", "t0_LocalName", [], "T@LocalName"], ["declare-fun", "t1_LocalName", [], "T@LocalName"], ["declare-fun", "t2_LocalName", [], "T@LocalName"], ["declare-fun", "t3_LocalName", [], "T@LocalName"], ["declare-fun", "t4_LocalName", [], "T@LocalName"], ["declare-fun", "t5_LocalName", [], "T@LocalName"], ["declare-fun", "t6_LocalName", [], "T@LocalName"], ["declare-fun", "t7_LocalName", [], "T@LocalName"], ["declare-fun", "t8_LocalName", [], "T@LocalName"], ["declare-fun", "t9_LocalName", [], "T@LocalName"], ["declare-fun", "t10_LocalName", [], "T@LocalName"], ["declare-fun", "t11_LocalName", [], "T@LocalName"], ["declare-fun", "t12_LocalName", [], "T@LocalName"], ["declare-fun", "t13_LocalName", [], "T@LocalName"], ["declare-fun", "t14_LocalName", [], "T@LocalName"], ["declare-fun", "t15_LocalName", [], "T@LocalName"], ["declare-fun", "t16_LocalName", [], "T@LocalName"], ["assert", ["distinct", "t0_LocalName", "t1_LocalName", "t2_LocalName", "t3_LocalName", "t4_LocalName", "t5_LocalName", "t6_LocalName", "t7_LocalName", "t8_LocalName", "t9_LocalName", "t10_LocalName", "t11_LocalName", "t12_LocalName", "t13_LocalName", "t14_LocalName", "t15_LocalName", "t16_LocalName"]], ["declare-fun", "ControlFlow", ["Int", "Int"], "Int"], ["declare-fun", "%lbl%+0", [], "Bool"], ["declare-fun", "%lbl%+1", [], "Bool"], ["declare-fun", "inline$IsPrefix0$1$srcPath@0", [], "T@Path"], ["declare-fun", "%lbl%@2", [], "Bool"], ["declare-fun", "%lbl%+3", [], "Bool"], ["declare-fun", "%lbl%+4", [], "Bool"], ["declare-fun", "inline$IsPrefix0$0$srcPath@0", [], "T@Path"], ["declare-fun", "%lbl%@5", [], "Bool"], ["declare-fun", "%lbl%+6", [], "Bool"], ["declare-fun", "%lbl%+7", [], "Bool"], ["declare-fun", "|inline$UpdateValueMax$2$dstValue'@1|", [], "T@Value"], ["declare-fun", "inline$UpdateValueMax$2$dstValue@0", [], "T@Value"], ["declare-fun", "inline$UpdateValueMax$2$e@0", [], "T@Edge"], ["declare-fun", "inline$UpdateValueMax$2$srcValue@0", [], "T@Value"], ["declare-fun", "%lbl%+8", [], "Bool"], ["declare-fun", "inline$UpdateValueMax$2$srcPath@0", [], "T@Path"], ["declare-fun", "inline$UpdateValue0$2$dstPath@0", [], "T@Path"], ["declare-fun", "%lbl%+9", [], "Bool"], ["declare-fun", "inline$UpdateValueMax$2$dstPath@0", [], "T@Path"], ["declare-fun", "%lbl%+10", [], "Bool"], ["declare-fun", "%lbl%+11", [], "Bool"], ["declare-fun", "inline$UpdateValue0$2$dstValue@0", [], "T@Value"], ["declare-fun", "%lbl%+12", [], "Bool"], ["declare-fun", "%lbl%+13", [], "Bool"], ["declare-fun", "|inline$WriteRef$0$to'@3|", [], "T@Reference"], ["declare-fun", "rs_TestReference_T", [], "T@ResourceStore"], ["declare-fun", "%lbl%+14", [], "Bool"], ["declare-fun", "%lbl%+15", [], "Bool"], ["declare-fun", "%lbl%+16", [], "Bool"], ["declare-fun", "|inline$DeepUpdateReference$0$dst'@2|", [], "T@Reference"], ["declare-fun", "arg0", [], "T@Reference"], ["declare-fun", "|inline$UpdateValueMax$1$dstValue'|", [], "T@Value"], ["declare-fun", "%lbl%+17", [], "Bool"], ["declare-fun", "|inline$UpdateValueMax$1$dstValue'@1|", [], "T@Value"], ["declare-fun", "inline$UpdateValueMax$1$dstValue@0", [], "T@Value"], ["declare-fun", "inline$UpdateValueMax$1$e@0", [], "T@Edge"], ["declare-fun", "inline$UpdateValueMax$1$srcValue@0", [], "T@Value"], ["declare-fun", "%lbl%+18", [], "Bool"], ["declare-fun", "inline$UpdateValueMax$1$srcPath@0", [], "T@Path"], ["declare-fun", "inline$UpdateValue0$1$dstPath@0", [], "T@Path"], ["declare-fun", "%lbl%+19", [], "Bool"], ["declare-fun", "inline$UpdateValueMax$1$dstPath@0", [], "T@Path"], ["declare-fun", "inline$UpdateValue0$1$dstValue@0", [], "T@Value"], ["declare-fun", "%lbl%+20", [], "Bool"], ["declare-fun", "%lbl%+21", [], "Bool"], ["declare-fun", "%lbl%+22", [], "Bool"], ["declare-fun", "%lbl%+23", [], "Bool"], ["declare-fun", "inline$IsPrefixMax$1$isPrefix@1", [], "Bool"], ["declare-fun", "%lbl%+24", [], "Bool"], ["declare-fun", "%lbl%+25", [], "Bool"], ["declare-fun", "inline$IsPrefix0$1$isPrefix@1", [], "Bool"], ["declare-fun", "%lbl%+26", [], "Bool"], ["declare-fun", "%lbl%+27", [], "Bool"], ["declare-fun", "inline$IsPrefixMax$1$dstPath@0", [], "T@Path"], ["declare-fun", "%lbl%+28", [], "Bool"], ["declare-fun", "%lbl%+29", [], "Bool"], ["declare-fun", "inline$IsPrefixMax$1$srcPath@0", [], "T@Path"], ["declare-fun", "%lbl%+30", [], "Bool"], ["declare-fun", "%lbl%+31", [], "Bool"], ["declare-fun", "%lbl%+32", [], "Bool"], ["declare-fun", "%lbl%+33", [], "Bool"], ["declare-fun", "%lbl%+34", [], "Bool"], ["declare-fun", "%lbl%+35", [], "Bool"], ["declare-fun", "%lbl%+36", [], "Bool"], ["declare-fun", "%lbl%+37", [], "Bool"], ["declare-fun", "%lbl%+38", [], "Bool"], ["declare-fun", "|inline$DeepUpdateReference$0$dst'@1|", [], "T@Reference"], ["declare-fun", "|inline$UpdateValueMax$0$dstValue'|", [], "T@Value"], ["declare-fun", "%lbl%+39", [], "Bool"], ["declare-fun", "|inline$UpdateValueMax$0$dstValue'@1|", [], "T@Value"], ["declare-fun", "inline$UpdateValueMax$0$dstValue@0", [], "T@Value"], ["declare-fun", "inline$UpdateValueMax$0$e@0", [], "T@Edge"], ["declare-fun", "inline$UpdateValueMax$0$srcValue@0", [], "T@Value"], ["declare-fun", "%lbl%+40", [], "Bool"], ["declare-fun", "inline$UpdateValueMax$0$srcPath@0", [], "T@Path"], ["declare-fun", "inline$UpdateValue0$0$dstPath@0", [], "T@Path"], ["declare-fun", "%lbl%+41", [], "Bool"], ["declare-fun", "inline$UpdateValueMax$0$dstPath@0", [], "T@Path"], ["declare-fun", "inline$UpdateValue0$0$dstValue@0", [], "T@Value"], ["declare-fun", "%lbl%+42", [], "Bool"], ["declare-fun", "%lbl%+43", [], "Bool"], ["declare-fun", "%lbl%+44", [], "Bool"], ["declare-fun", "%lbl%+45", [], "Bool"], ["declare-fun", "inline$IsPrefixMax$0$isPrefix@1", [], "Bool"], ["declare-fun", "%lbl%+46", [], "Bool"], ["declare-fun", "%lbl%+47", [], "Bool"], ["declare-fun", "inline$IsPrefix0$0$isPrefix@1", [], "Bool"], ["declare-fun", "%lbl%+48", [], "Bool"], ["declare-fun", "%lbl%+49", [], "Bool"], ["declare-fun", "inline$IsPrefixMax$0$dstPath@0", [], "T@Path"], ["declare-fun", "%lbl%+50", [], "Bool"], ["declare-fun", "%lbl%+51", [], "Bool"], ["declare-fun", "inline$IsPrefixMax$0$srcPath@0", [], "T@Path"], ["declare-fun", "%lbl%+52", [], "Bool"], ["declare-fun", "%lbl%+53", [], "Bool"], ["declare-fun", "%lbl%+54", [], "Bool"], ["declare-fun", "%lbl%+55", [], "Bool"], ["declare-fun", "%lbl%+56", [], "Bool"], ["declare-fun", "%lbl%+57", [], "Bool"], ["declare-fun", "%lbl%+58", [], "Bool"], ["declare-fun", "%lbl%+59", [], "Bool"], ["declare-fun", "%lbl%+60", [], "Bool"], ["declare-fun", "|inline$WriteRef$0$to'@2|", [], "T@Reference"], ["declare-fun", "inline$LdConst$0$ret@1", [], "T@Value"], ["declare-fun", "%lbl%+61", [], "Bool"], ["declare-fun", "|inline$WriteRef$0$to'@1|", [], "T@Reference"], ["declare-fun", "%lbl%+62", [], "Bool"], ["declare-fun", "%lbl%+63", [], "Bool"], ["declare-fun", "|c'|", [], "Int"], ["declare-fun", "c", [], "Int"], ["declare-fun", "%lbl%+64", [], "Bool"], ["push", "1"], ["set-info", ":boogie-vc-id", "TestReference_mut_b"], ["assert", ["not", ["=>", ["=", ["ControlFlow", "0", "0"], "16187"], ["let", [["inline$UpdateValue0$1$anon3_Else_correct", ["=>", ["and", "%lbl%+0", "true"], "true"]]], ["let", [["inline$IsPrefix0$1$anon5_Else_correct", ["=>", ["and", "%lbl%+1", "true"], ["=>", ["not", ["=", "inline$IsPrefix0$1$srcPath@0", "Nil"]], ["or", "%lbl%@2", ["=>", ["=", ["ControlFlow", "0", "4205"], ["-", "0", "16915"]], "false"]]]]]], ["let", [["inline$UpdateValue0$0$anon3_Else_correct", ["=>", ["and", "%lbl%+3", "true"], "true"]]], ["let", [["inline$IsPrefix0$0$anon5_Else_correct", ["=>", ["and", "%lbl%+4", "true"], ["=>", ["not", ["=", "inline$IsPrefix0$0$srcPath@0", "Nil"]], ["or", "%lbl%@5", ["=>", ["=", ["ControlFlow", "0", "3647"], ["-", "0", "16619"]], "false"]]]]]], ["let", [["inline$DeepUpdateGlobal$0$anon2_Then$1_correct", ["=>", ["and", "%lbl%+6", "true"], "true"]]], ["let", [["inline$UpdateValueMax$2$anon3_Else$1_correct", ["=>", ["and", "%lbl%+7", "true"], ["=>", ["and", ["=", "|inline$UpdateValueMax$2$dstValue'@1|", ["Map", ["store", ["|m#Map|", "inline$UpdateValueMax$2$dstValue@0"], "inline$UpdateValueMax$2$e@0", "inline$UpdateValueMax$2$srcValue@0"]]], ["=", ["ControlFlow", "0", "4883"], "4919"]], "inline$DeepUpdateGlobal$0$anon2_Then$1_correct"]]]], ["let", [["inline$UpdateValue0$2$anon3_Then_correct", ["=>", ["and", "%lbl%+8", "true"], ["=>", ["and", ["=", "inline$UpdateValueMax$2$srcPath@0", "inline$UpdateValue0$2$dstPath@0"], ["=", ["ControlFlow", "0", "4863"], "4883"]], "inline$UpdateValueMax$2$anon3_Else$1_correct"]]]], ["let", [["inline$UpdateValueMax$2$anon3_Then_correct", ["=>", ["and", "%lbl%+9", "true"], ["=>", ["and", ["=", "inline$UpdateValueMax$2$srcPath@0", "inline$UpdateValueMax$2$dstPath@0"], ["=", ["ControlFlow", "0", "4893"], "4919"]], "inline$DeepUpdateGlobal$0$anon2_Then$1_correct"]]]], ["let", [["inline$UpdateValue0$2$anon3_Else_correct", ["=>", ["and", "%lbl%+10", "true"], "true"]]], ["let", [["inline$UpdateValue0$2$Entry_correct", ["=>", ["and", "%lbl%+11", "true"], ["=>", ["and", ["=", "inline$UpdateValue0$2$dstPath@0", ["Cons", "inline$UpdateValueMax$2$dstPath@0", "inline$UpdateValueMax$2$e@0"]], ["=", "inline$UpdateValue0$2$dstValue@0", ["select", ["|m#Map|", "inline$UpdateValueMax$2$dstValue@0"], "inline$UpdateValueMax$2$e@0"]]], ["and", ["=>", ["=", ["ControlFlow", "0", "4841"], "4863"], "inline$UpdateValue0$2$anon3_Then_correct"], ["=>", ["=", ["ControlFlow", "0", "4841"], "4853"], "inline$UpdateValue0$2$anon3_Else_correct"]]]]]], ["let", [["inline$UpdateValueMax$2$anon3_Else_correct", ["=>", ["and", "%lbl%+12", "true"], ["=>", ["and", ["not", ["=", "inline$UpdateValueMax$2$srcPath@0", "inline$UpdateValueMax$2$dstPath@0"]], ["=", ["ControlFlow", "0", "4869"], "4841"]], "inline$UpdateValue0$2$Entry_correct"]]]], ["let", [["inline$UpdateValueMax$2$Entry_correct", ["=>", ["and", "%lbl%+13", "true"], ["=>", ["and", ["and", ["=", "inline$UpdateValueMax$2$srcPath@0", ["|p#GlobalReference|", "|inline$WriteRef$0$to'@3|"]], ["=", "inline$UpdateValueMax$2$srcValue@0", ["|v#GlobalReference|", "|inline$WriteRef$0$to'@3|"]]], ["and", ["=", "inline$UpdateValueMax$2$dstPath@0", "Nil"], ["=", "inline$UpdateValueMax$2$dstValue@0", ["select", ["|contents#ResourceStore|", "rs_TestReference_T"], ["|a#GlobalReference|", "|inline$WriteRef$0$to'@3|"]]]]], ["and", ["=>", ["=", ["ControlFlow", "0", "4762"], "4893"], "inline$UpdateValueMax$2$anon3_Then_correct"], ["=>", ["=", ["ControlFlow", "0", "4762"], "4869"], "inline$UpdateValueMax$2$anon3_Else_correct"]]]]]], ["let", [["inline$DeepUpdateGlobal$0$anon2_Then_correct", ["=>", ["and", "%lbl%+14", "true"], ["=>", ["and", ["and", ["is-GlobalReference", "|inline$WriteRef$0$to'@3|"], ["=", "TestReference_T", ["|t#GlobalReference|", "|inline$WriteRef$0$to'@3|"]]], ["=", ["ControlFlow", "0", "4899"], "4762"]], "inline$UpdateValueMax$2$Entry_correct"]]]], ["let", [["inline$DeepUpdateGlobal$0$anon2_Else_correct", ["=>", ["and", "%lbl%+15", "true"], "true"]]], ["let", [["inline$DeepUpdateReference$0$anon9_Then$1_correct", ["=>", ["and", "%lbl%+16", "true"], ["=>", ["=", "|inline$DeepUpdateReference$0$dst'@2|", ["LocalReference", ["|c#LocalReference|", "arg0"], ["|l#LocalReference|", "arg0"], ["|p#LocalReference|", "arg0"], "|inline$UpdateValueMax$1$dstValue'|"]], ["and", ["=>", ["=", ["ControlFlow", "0", "4519"], "4899"], "inline$DeepUpdateGlobal$0$anon2_Then_correct"], ["=>", ["=", ["ControlFlow", "0", "4519"], "4649"], "inline$DeepUpdateGlobal$0$anon2_Else_correct"]]]]]], ["let", [["inline$UpdateValueMax$1$anon3_Else$1_correct", ["=>", ["and", "%lbl%+17", "true"], ["=>", ["and", ["=", "|inline$UpdateValueMax$1$dstValue'@1|", ["Map", ["store", ["|m#Map|", "inline$UpdateValueMax$1$dstValue@0"], "inline$UpdateValueMax$1$e@0", "inline$UpdateValueMax$1$srcValue@0"]]], ["=", ["ControlFlow", "0", "4485"], "4519"]], "inline$DeepUpdateReference$0$anon9_Then$1_correct"]]]], ["let", [["inline$UpdateValue0$1$anon3_Then_correct", ["=>", ["and", "%lbl%+18", "true"], ["=>", ["and", ["=", "inline$UpdateValueMax$1$srcPath@0", "inline$UpdateValue0$1$dstPath@0"], ["=", ["ControlFlow", "0", "4465"], "4485"]], "inline$UpdateValueMax$1$anon3_Else$1_correct"]]]], ["let", [["inline$UpdateValue0$1$Entry_correct", ["=>", ["and", "%lbl%+19", "true"], ["=>", ["and", ["=", "inline$UpdateValue0$1$dstPath@0", ["Cons", "inline$UpdateValueMax$1$dstPath@0", "inline$UpdateValueMax$1$e@0"]], ["=", "inline$UpdateValue0$1$dstValue@0", ["select", ["|m#Map|", "inline$UpdateValueMax$1$dstValue@0"], "inline$UpdateValueMax$1$e@0"]]], ["and", ["=>", ["=", ["ControlFlow", "0", "4443"], "4465"], "inline$UpdateValue0$1$anon3_Then_correct"], ["=>", ["=", ["ControlFlow", "0", "4443"], "4455"], "inline$UpdateValue0$1$anon3_Else_correct"]]]]]], ["let", [["inline$UpdateValueMax$1$anon3_Else_correct", ["=>", ["and", "%lbl%+20", "true"], ["=>", ["and", ["not", ["=", "inline$UpdateValueMax$1$srcPath@0", "inline$UpdateValueMax$1$dstPath@0"]], ["=", ["ControlFlow", "0", "4471"], "4443"]], "inline$UpdateValue0$1$Entry_correct"]]]], ["let", [["inline$UpdateValueMax$1$anon3_Then_correct", ["=>", ["and", "%lbl%+21", "true"], ["=>", ["and", ["=", "inline$UpdateValueMax$1$srcPath@0", "inline$UpdateValueMax$1$dstPath@0"], ["=", ["ControlFlow", "0", "4495"], "4519"]], "inline$DeepUpdateReference$0$anon9_Then$1_correct"]]]], ["let", [["inline$UpdateValueMax$1$Entry_correct", ["=>", ["and", "%lbl%+22", "true"], ["=>", ["and", ["and", ["=", "inline$UpdateValueMax$1$srcPath@0", ["|p#LocalReference|", "|inline$WriteRef$0$to'@3|"]], ["=", "inline$UpdateValueMax$1$srcValue@0", ["|v#LocalReference|", "|inline$WriteRef$0$to'@3|"]]], ["and", ["=", "inline$UpdateValueMax$1$dstPath@0", ["|p#LocalReference|", "arg0"]], ["=", "inline$UpdateValueMax$1$dstValue@0", ["|v#LocalReference|", "arg0"]]]], ["and", ["=>", ["=", ["ControlFlow", "0", "4364"], "4495"], "inline$UpdateValueMax$1$anon3_Then_correct"], ["=>", ["=", ["ControlFlow", "0", "4364"], "4471"], "inline$UpdateValueMax$1$anon3_Else_correct"]]]]]], ["let", [["inline$DeepUpdateReference$0$anon9_Then_correct", ["=>", ["and", "%lbl%+23", "true"], ["=>", ["and", "inline$IsPrefixMax$1$isPrefix@1", ["=", ["ControlFlow", "0", "4501"], "4364"]], "inline$UpdateValueMax$1$Entry_correct"]]]], ["let", [["inline$DeepUpdateReference$0$anon9_Else_correct", ["=>", ["and", "%lbl%+24", "true"], ["=>", ["not", "inline$IsPrefixMax$1$isPrefix@1"], ["and", ["=>", ["=", ["ControlFlow", "0", "4267"], "4899"], "inline$DeepUpdateGlobal$0$anon2_Then_correct"], ["=>", ["=", ["ControlFlow", "0", "4267"], "4649"], "inline$DeepUpdateGlobal$0$anon2_Else_correct"]]]]]], ["let", [["inline$IsPrefixMax$1$anon5_Else$1_correct", ["=>", ["and", "%lbl%+25", "true"], ["=>", ["and", ["=>", "inline$IsPrefixMax$1$isPrefix@1", "inline$IsPrefix0$1$isPrefix@1"], ["=>", "inline$IsPrefix0$1$isPrefix@1", "inline$IsPrefixMax$1$isPrefix@1"]], ["and", ["=>", ["=", ["ControlFlow", "0", "4233"], "4501"], "inline$DeepUpdateReference$0$anon9_Then_correct"], ["=>", ["=", ["ControlFlow", "0", "4233"], "4267"], "inline$DeepUpdateReference$0$anon9_Else_correct"]]]]]], ["let", [["inline$IsPrefix0$1$anon5_Then_correct", ["=>", ["and", "%lbl%+26", "true"], ["=>", ["=", "inline$IsPrefix0$1$srcPath@0", "Nil"], ["=>", ["and", ["and", ["=>", "inline$IsPrefix0$1$isPrefix@1", "false"], ["=>", "false", "inline$IsPrefix0$1$isPrefix@1"]], ["=", ["ControlFlow", "0", "4215"], "4233"]], "inline$IsPrefixMax$1$anon5_Else$1_correct"]]]]], ["let", [["inline$IsPrefix0$1$anon4_Else_correct", ["=>", ["and", "%lbl%+27", "true"], ["=>", ["not", ["=", "inline$IsPrefix0$1$srcPath@0", "inline$IsPrefixMax$1$dstPath@0"]], ["and", ["=>", ["=", ["ControlFlow", "0", "4195"], "4215"], "inline$IsPrefix0$1$anon5_Then_correct"], ["=>", ["=", ["ControlFlow", "0", "4195"], "4205"], "inline$IsPrefix0$1$anon5_Else_correct"]]]]]], ["let", [["inline$IsPrefix0$1$anon4_Then_correct", ["=>", ["and", "%lbl%+28", "true"], ["=>", ["=", "inline$IsPrefix0$1$srcPath@0", "inline$IsPrefixMax$1$dstPath@0"], ["=>", ["and", ["and", ["=>", "inline$IsPrefix0$1$isPrefix@1", "true"], ["=>", "true", "inline$IsPrefix0$1$isPrefix@1"]], ["=", ["ControlFlow", "0", "4225"], "4233"]], "inline$IsPrefixMax$1$anon5_Else$1_correct"]]]]], ["let", [["inline$IsPrefix0$1$Entry_correct", ["=>", ["and", "%lbl%+29", "true"], ["=>", ["=", "inline$IsPrefix0$1$srcPath@0", ["|p#Cons|", "inline$IsPrefixMax$1$srcPath@0"]], ["and", ["=>", ["=", ["ControlFlow", "0", "4185"], "4225"], "inline$IsPrefix0$1$anon4_Then_correct"], ["=>", ["=", ["ControlFlow", "0", "4185"], "4195"], "inline$IsPrefix0$1$anon4_Else_correct"]]]]]], ["let", [["inline$IsPrefixMax$1$anon5_Else_correct", ["=>", ["and", "%lbl%+30", "true"], ["=>", ["and", ["not", ["=", "inline$IsPrefixMax$1$srcPath@0", "Nil"]], ["=", ["ControlFlow", "0", "4231"], "4185"]], "inline$IsPrefix0$1$Entry_correct"]]]], ["let", [["inline$IsPrefixMax$1$anon5_Then_correct", ["=>", ["and", "%lbl%+31", "true"], ["=>", ["=", "inline$IsPrefixMax$1$srcPath@0", "Nil"], ["=>", ["and", ["=>", "inline$IsPrefixMax$1$isPrefix@1", "false"], ["=>", "false", "inline$IsPrefixMax$1$isPrefix@1"]], ["and", ["=>", ["=", ["ControlFlow", "0", "4243"], "4501"], "inline$DeepUpdateReference$0$anon9_Then_correct"], ["=>", ["=", ["ControlFlow", "0", "4243"], "4267"], "inline$DeepUpdateReference$0$anon9_Else_correct"]]]]]]], ["let", [["inline$IsPrefixMax$1$anon4_Else_correct", ["=>", ["and", "%lbl%+32", "true"], ["=>", ["not", ["=", "inline$IsPrefixMax$1$srcPath@0", "inline$IsPrefixMax$1$dstPath@0"]], ["and", ["=>", ["=", ["ControlFlow", "0", "4110"], "4243"], "inline$IsPrefixMax$1$anon5_Then_correct"], ["=>", ["=", ["ControlFlow", "0", "4110"], "4231"], "inline$IsPrefixMax$1$anon5_Else_correct"]]]]]], ["let", [["inline$IsPrefixMax$1$anon4_Then_correct", ["=>", ["and", "%lbl%+33", "true"], ["=>", ["=", "inline$IsPrefixMax$1$srcPath@0", "inline$IsPrefixMax$1$dstPath@0"], ["=>", ["and", ["=>", "inline$IsPrefixMax$1$isPrefix@1", "true"], ["=>", "true", "inline$IsPrefixMax$1$isPrefix@1"]], ["and", ["=>", ["=", ["ControlFlow", "0", "4253"], "4501"], "inline$DeepUpdateReference$0$anon9_Then_correct"], ["=>", ["=", ["ControlFlow", "0", "4253"], "4267"], "inline$DeepUpdateReference$0$anon9_Else_correct"]]]]]]], ["let", [["inline$IsPrefixMax$1$Entry_correct", ["=>", ["and", "%lbl%+34", "true"], ["=>", ["and", ["=", "inline$IsPrefixMax$1$dstPath@0", ["|p#LocalReference|", "arg0"]], ["=", "inline$IsPrefixMax$1$srcPath@0", ["|p#LocalReference|", "|inline$WriteRef$0$to'@3|"]]], ["and", ["=>", ["=", ["ControlFlow", "0", "4100"], "4253"], "inline$IsPrefixMax$1$anon4_Then_correct"], ["=>", ["=", ["ControlFlow", "0", "4100"], "4110"], "inline$IsPrefixMax$1$anon4_Else_correct"]]]]]], ["let", [["inline$DeepUpdateReference$0$anon8_Then_correct", ["=>", ["and", "%lbl%+35", "true"], ["=>", ["and", ["and", ["and", ["is-LocalReference", "arg0"], ["=", ["|c#LocalReference|", "|inline$WriteRef$0$to'@3|"], ["|c#LocalReference|", "arg0"]]], ["=", ["|l#LocalReference|", "|inline$WriteRef$0$to'@3|"], ["|l#LocalReference|", "arg0"]]], ["=", ["ControlFlow", "0", "4259"], "4100"]], "inline$IsPrefixMax$1$Entry_correct"]]]], ["let", [["inline$DeepUpdateReference$0$anon8_Else_correct", ["=>", ["and", "%lbl%+36", "true"], ["=>", ["not", ["and", ["and", ["is-LocalReference", "arg0"], ["=", ["|c#LocalReference|", "|inline$WriteRef$0$to'@3|"], ["|c#LocalReference|", "arg0"]]], ["=", ["|l#LocalReference|", "|inline$WriteRef$0$to'@3|"], ["|l#LocalReference|", "arg0"]]]], ["and", ["=>", ["=", ["ControlFlow", "0", "3999"], "4899"], "inline$DeepUpdateGlobal$0$anon2_Then_correct"], ["=>", ["=", ["ControlFlow", "0", "3999"], "4649"], "inline$DeepUpdateGlobal$0$anon2_Else_correct"]]]]]], ["let", [["inline$DeepUpdateReference$0$anon7_Then_correct", ["=>", ["and", "%lbl%+37", "true"], ["=>", ["is-LocalReference", "|inline$WriteRef$0$to'@3|"], ["and", ["=>", ["=", ["ControlFlow", "0", "3967"], "4259"], "inline$DeepUpdateReference$0$anon8_Then_correct"], ["=>", ["=", ["ControlFlow", "0", "3967"], "3999"], "inline$DeepUpdateReference$0$anon8_Else_correct"]]]]]], ["let", [["inline$DeepUpdateReference$0$anon11_Then$1_correct", ["=>", ["and", "%lbl%+38", "true"], ["=>", ["=", "|inline$DeepUpdateReference$0$dst'@1|", ["GlobalReference", ["|a#GlobalReference|", "arg0"], ["|t#GlobalReference|", "arg0"], ["|p#GlobalReference|", "arg0"], "|inline$UpdateValueMax$0$dstValue'|"]], ["and", ["=>", ["=", ["ControlFlow", "0", "3961"], "4899"], "inline$DeepUpdateGlobal$0$anon2_Then_correct"], ["=>", ["=", ["ControlFlow", "0", "3961"], "4649"], "inline$DeepUpdateGlobal$0$anon2_Else_correct"]]]]]], ["let", [["inline$UpdateValueMax$0$anon3_Else$1_correct", ["=>", ["and", "%lbl%+39", "true"], ["=>", ["and", ["=", "|inline$UpdateValueMax$0$dstValue'@1|", ["Map", ["store", ["|m#Map|", "inline$UpdateValueMax$0$dstValue@0"], "inline$UpdateValueMax$0$e@0", "inline$UpdateValueMax$0$srcValue@0"]]], ["=", ["ControlFlow", "0", "3927"], "3961"]], "inline$DeepUpdateReference$0$anon11_Then$1_correct"]]]], ["let", [["inline$UpdateValue0$0$anon3_Then_correct", ["=>", ["and", "%lbl%+40", "true"], ["=>", ["and", ["=", "inline$UpdateValueMax$0$srcPath@0", "inline$UpdateValue0$0$dstPath@0"], ["=", ["ControlFlow", "0", "3907"], "3927"]], "inline$UpdateValueMax$0$anon3_Else$1_correct"]]]], ["let", [["inline$UpdateValue0$0$Entry_correct", ["=>", ["and", "%lbl%+41", "true"], ["=>", ["and", ["=", "inline$UpdateValue0$0$dstPath@0", ["Cons", "inline$UpdateValueMax$0$dstPath@0", "inline$UpdateValueMax$0$e@0"]], ["=", "inline$UpdateValue0$0$dstValue@0", ["select", ["|m#Map|", "inline$UpdateValueMax$0$dstValue@0"], "inline$UpdateValueMax$0$e@0"]]], ["and", ["=>", ["=", ["ControlFlow", "0", "3885"], "3907"], "inline$UpdateValue0$0$anon3_Then_correct"], ["=>", ["=", ["ControlFlow", "0", "3885"], "3897"], "inline$UpdateValue0$0$anon3_Else_correct"]]]]]], ["let", [["inline$UpdateValueMax$0$anon3_Else_correct", ["=>", ["and", "%lbl%+42", "true"], ["=>", ["and", ["not", ["=", "inline$UpdateValueMax$0$srcPath@0", "inline$UpdateValueMax$0$dstPath@0"]], ["=", ["ControlFlow", "0", "3913"], "3885"]], "inline$UpdateValue0$0$Entry_correct"]]]], ["let", [["inline$UpdateValueMax$0$anon3_Then_correct", ["=>", ["and", "%lbl%+43", "true"], ["=>", ["and", ["=", "inline$UpdateValueMax$0$srcPath@0", "inline$UpdateValueMax$0$dstPath@0"], ["=", ["ControlFlow", "0", "3937"], "3961"]], "inline$DeepUpdateReference$0$anon11_Then$1_correct"]]]], ["let", [["inline$UpdateValueMax$0$Entry_correct", ["=>", ["and", "%lbl%+44", "true"], ["=>", ["and", ["and", ["=", "inline$UpdateValueMax$0$srcPath@0", ["|p#GlobalReference|", "|inline$WriteRef$0$to'@3|"]], ["=", "inline$UpdateValueMax$0$srcValue@0", ["|v#GlobalReference|", "|inline$WriteRef$0$to'@3|"]]], ["and", ["=", "inline$UpdateValueMax$0$dstPath@0", ["|p#GlobalReference|", "arg0"]], ["=", "inline$UpdateValueMax$0$dstValue@0", ["|v#GlobalReference|", "arg0"]]]], ["and", ["=>", ["=", ["ControlFlow", "0", "3806"], "3937"], "inline$UpdateValueMax$0$anon3_Then_correct"], ["=>", ["=", ["ControlFlow", "0", "3806"], "3913"], "inline$UpdateValueMax$0$anon3_Else_correct"]]]]]], ["let", [["inline$DeepUpdateReference$0$anon11_Then_correct", ["=>", ["and", "%lbl%+45", "true"], ["=>", ["and", "inline$IsPrefixMax$0$isPrefix@1", ["=", ["ControlFlow", "0", "3943"], "3806"]], "inline$UpdateValueMax$0$Entry_correct"]]]], ["let", [["inline$DeepUpdateReference$0$anon11_Else_correct", ["=>", ["and", "%lbl%+46", "true"], ["=>", ["not", "inline$IsPrefixMax$0$isPrefix@1"], ["and", ["=>", ["=", ["ControlFlow", "0", "3709"], "4899"], "inline$DeepUpdateGlobal$0$anon2_Then_correct"], ["=>", ["=", ["ControlFlow", "0", "3709"], "4649"], "inline$DeepUpdateGlobal$0$anon2_Else_correct"]]]]]], ["let", [["inline$IsPrefixMax$0$anon5_Else$1_correct", ["=>", ["and", "%lbl%+47", "true"], ["=>", ["and", ["=>", "inline$IsPrefixMax$0$isPrefix@1", "inline$IsPrefix0$0$isPrefix@1"], ["=>", "inline$IsPrefix0$0$isPrefix@1", "inline$IsPrefixMax$0$isPrefix@1"]], ["and", ["=>", ["=", ["ControlFlow", "0", "3675"], "3943"], "inline$DeepUpdateReference$0$anon11_Then_correct"], ["=>", ["=", ["ControlFlow", "0", "3675"], "3709"], "inline$DeepUpdateReference$0$anon11_Else_correct"]]]]]], ["let", [["inline$IsPrefix0$0$anon5_Then_correct", ["=>", ["and", "%lbl%+48", "true"], ["=>", ["=", "inline$IsPrefix0$0$srcPath@0", "Nil"], ["=>", ["and", ["and", ["=>", "inline$IsPrefix0$0$isPrefix@1", "false"], ["=>", "false", "inline$IsPrefix0$0$isPrefix@1"]], ["=", ["ControlFlow", "0", "3657"], "3675"]], "inline$IsPrefixMax$0$anon5_Else$1_correct"]]]]], ["let", [["inline$IsPrefix0$0$anon4_Else_correct", ["=>", ["and", "%lbl%+49", "true"], ["=>", ["not", ["=", "inline$IsPrefix0$0$srcPath@0", "inline$IsPrefixMax$0$dstPath@0"]], ["and", ["=>", ["=", ["ControlFlow", "0", "3637"], "3657"], "inline$IsPrefix0$0$anon5_Then_correct"], ["=>", ["=", ["ControlFlow", "0", "3637"], "3647"], "inline$IsPrefix0$0$anon5_Else_correct"]]]]]], ["let", [["inline$IsPrefix0$0$anon4_Then_correct", ["=>", ["and", "%lbl%+50", "true"], ["=>", ["=", "inline$IsPrefix0$0$srcPath@0", "inline$IsPrefixMax$0$dstPath@0"], ["=>", ["and", ["and", ["=>", "inline$IsPrefix0$0$isPrefix@1", "true"], ["=>", "true", "inline$IsPrefix0$0$isPrefix@1"]], ["=", ["ControlFlow", "0", "3667"], "3675"]], "inline$IsPrefixMax$0$anon5_Else$1_correct"]]]]], ["let", [["inline$IsPrefix0$0$Entry_correct", ["=>", ["and", "%lbl%+51", "true"], ["=>", ["=", "inline$IsPrefix0$0$srcPath@0", ["|p#Cons|", "inline$IsPrefixMax$0$srcPath@0"]], ["and", ["=>", ["=", ["ControlFlow", "0", "3627"], "3667"], "inline$IsPrefix0$0$anon4_Then_correct"], ["=>", ["=", ["ControlFlow", "0", "3627"], "3637"], "inline$IsPrefix0$0$anon4_Else_correct"]]]]]], ["let", [["inline$IsPrefixMax$0$anon5_Else_correct", ["=>", ["and", "%lbl%+52", "true"], ["=>", ["and", ["not", ["=", "inline$IsPrefixMax$0$srcPath@0", "Nil"]], ["=", ["ControlFlow", "0", "3673"], "3627"]], "inline$IsPrefix0$0$Entry_correct"]]]], ["let", [["inline$IsPrefixMax$0$anon5_Then_correct", ["=>", ["and", "%lbl%+53", "true"], ["=>", ["=", "inline$IsPrefixMax$0$srcPath@0", "Nil"], ["=>", ["and", ["=>", "inline$IsPrefixMax$0$isPrefix@1", "false"], ["=>", "false", "inline$IsPrefixMax$0$isPrefix@1"]], ["and", ["=>", ["=", ["ControlFlow", "0", "3685"], "3943"], "inline$DeepUpdateReference$0$anon11_Then_correct"], ["=>", ["=", ["ControlFlow", "0", "3685"], "3709"], "inline$DeepUpdateReference$0$anon11_Else_correct"]]]]]]], ["let", [["inline$IsPrefixMax$0$anon4_Else_correct", ["=>", ["and", "%lbl%+54", "true"], ["=>", ["not", ["=", "inline$IsPrefixMax$0$srcPath@0", "inline$IsPrefixMax$0$dstPath@0"]], ["and", ["=>", ["=", ["ControlFlow", "0", "3552"], "3685"], "inline$IsPrefixMax$0$anon5_Then_correct"], ["=>", ["=", ["ControlFlow", "0", "3552"], "3673"], "inline$IsPrefixMax$0$anon5_Else_correct"]]]]]], ["let", [["inline$IsPrefixMax$0$anon4_Then_correct", ["=>", ["and", "%lbl%+55", "true"], ["=>", ["=", "inline$IsPrefixMax$0$srcPath@0", "inline$IsPrefixMax$0$dstPath@0"], ["=>", ["and", ["=>", "inline$IsPrefixMax$0$isPrefix@1", "true"], ["=>", "true", "inline$IsPrefixMax$0$isPrefix@1"]], ["and", ["=>", ["=", ["ControlFlow", "0", "3695"], "3943"], "inline$DeepUpdateReference$0$anon11_Then_correct"], ["=>", ["=", ["ControlFlow", "0", "3695"], "3709"], "inline$DeepUpdateReference$0$anon11_Else_correct"]]]]]]], ["let", [["inline$IsPrefixMax$0$Entry_correct", ["=>", ["and", "%lbl%+56", "true"], ["=>", ["and", ["=", "inline$IsPrefixMax$0$dstPath@0", ["|p#GlobalReference|", "arg0"]], ["=", "inline$IsPrefixMax$0$srcPath@0", ["|p#GlobalReference|", "|inline$WriteRef$0$to'@3|"]]], ["and", ["=>", ["=", ["ControlFlow", "0", "3542"], "3695"], "inline$IsPrefixMax$0$anon4_Then_correct"], ["=>", ["=", ["ControlFlow", "0", "3542"], "3552"], "inline$IsPrefixMax$0$anon4_Else_correct"]]]]]], ["let", [["inline$DeepUpdateReference$0$anon10_Then_correct", ["=>", ["and", "%lbl%+57", "true"], ["=>", ["and", ["and", ["and", ["is-GlobalReference", "arg0"], ["=", ["|a#GlobalReference|", "|inline$WriteRef$0$to'@3|"], ["|a#GlobalReference|", "arg0"]]], ["=", ["|t#GlobalReference|", "|inline$WriteRef$0$to'@3|"], ["|t#GlobalReference|", "arg0"]]], ["=", ["ControlFlow", "0", "3701"], "3542"]], "inline$IsPrefixMax$0$Entry_correct"]]]], ["let", [["inline$DeepUpdateReference$0$anon10_Else_correct", ["=>", ["and", "%lbl%+58", "true"], ["=>", ["not", ["and", ["and", ["is-GlobalReference", "arg0"], ["=", ["|a#GlobalReference|", "|inline$WriteRef$0$to'@3|"], ["|a#GlobalReference|", "arg0"]]], ["=", ["|t#GlobalReference|", "|inline$WriteRef$0$to'@3|"], ["|t#GlobalReference|", "arg0"]]]], ["and", ["=>", ["=", ["ControlFlow", "0", "3441"], "4899"], "inline$DeepUpdateGlobal$0$anon2_Then_correct"], ["=>", ["=", ["ControlFlow", "0", "3441"], "4649"], "inline$DeepUpdateGlobal$0$anon2_Else_correct"]]]]]], ["let", [["inline$DeepUpdateReference$0$anon7_Else_correct", ["=>", ["and", "%lbl%+59", "true"], ["=>", ["not", ["is-LocalReference", "|inline$WriteRef$0$to'@3|"]], ["and", ["=>", ["=", ["ControlFlow", "0", "3409"], "3701"], "inline$DeepUpdateReference$0$anon10_Then_correct"], ["=>", ["=", ["ControlFlow", "0", "3409"], "3441"], "inline$DeepUpdateReference$0$anon10_Else_correct"]]]]]], ["let", [["inline$WriteRef$0$anon3_Else_correct", ["=>", ["and", "%lbl%+60", "true"], ["=>", ["not", ["is-GlobalReference", "arg0"]], ["=>", ["and", ["=", "|inline$WriteRef$0$to'@2|", ["LocalReference", ["|c#LocalReference|", "arg0"], ["|l#LocalReference|", "arg0"], ["|p#LocalReference|", "arg0"], "inline$LdConst$0$ret@1"]], ["=", "|inline$WriteRef$0$to'@3|", "|inline$WriteRef$0$to'@2|"]], ["and", ["=>", ["=", ["ControlFlow", "0", "3125"], "3967"], "inline$DeepUpdateReference$0$anon7_Then_correct"], ["=>", ["=", ["ControlFlow", "0", "3125"], "3409"], "inline$DeepUpdateReference$0$anon7_Else_correct"]]]]]]], ["let", [["inline$WriteRef$0$anon3_Then_correct", ["=>", ["and", "%lbl%+61", "true"], ["=>", ["is-GlobalReference", "arg0"], ["=>", ["and", ["=", "|inline$WriteRef$0$to'@1|", ["GlobalReference", ["|a#GlobalReference|", "arg0"], ["|t#GlobalReference|", "arg0"], ["|p#GlobalReference|", "arg0"], "inline$LdConst$0$ret@1"]], ["=", "|inline$WriteRef$0$to'@3|", "|inline$WriteRef$0$to'@1|"]], ["and", ["=>", ["=", ["ControlFlow", "0", "3147"], "3967"], "inline$DeepUpdateReference$0$anon7_Then_correct"], ["=>", ["=", ["ControlFlow", "0", "3147"], "3409"], "inline$DeepUpdateReference$0$anon7_Else_correct"]]]]]]], ["let", [["inline$LdConst$0$anon0_correct", ["=>", ["and", "%lbl%+62", "true"], ["=>", ["=", "inline$LdConst$0$ret@1", ["Integer", "0"]], ["and", ["=>", ["=", ["ControlFlow", "0", "2992"], "3147"], "inline$WriteRef$0$anon3_Then_correct"], ["=>", ["=", ["ControlFlow", "0", "2992"], "3125"], "inline$WriteRef$0$anon3_Else_correct"]]]]]], ["let", [["anon0_correct", ["=>", ["and", "%lbl%+63", "true"], ["=>", ["and", [">", "|c'|", "c"], ["=", ["ControlFlow", "0", "2998"], "2992"]], "inline$LdConst$0$anon0_correct"]]]], ["let", [["PreconditionGeneratedEntry_correct", ["=>", ["and", "%lbl%+64", "true"], ["=>", ["=", ["ControlFlow", "0", "16187"], "2998"], "anon0_correct"]]]], "PreconditionGeneratedEntry_correct"]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]], ["check-sat"], ["set-option", ":print-success", "false"], ["set-info", ":smt-lib-version", "2.0"], ["set-option", ":produce-models", "true"], ["set-option", ":AUTO_CONFIG", "false"], ["set-option", ":pp.bv_literals", "false"], ["set-option", ":MODEL.V2", "true"], ["set-option", ":smt.PHASE_SELECTION", "0"], ["set-option", ":smt.RESTART_STRATEGY", "0"], ["set-option", ":smt.RESTART_FACTOR", "|1.5|"], ["set-option", ":smt.ARITH.RANDOM_INITIAL_VALUE", "true"], ["set-option", ":smt.CASE_SPLIT", "3"], ["set-option", ":smt.DELAY_UNITS", "true"], ["set-option", ":NNF.SK_HACK", "true"], ["set-option", ":smt.MBQI", "false"], ["set-option", ":smt.QI.EAGER_THRESHOLD", "100"], ["set-option", ":TYPE_CHECK", "true"], ["set-option", ":smt.BV.REFLECT", "true"], ["set-option", ":model_compress", "false"], "; done setting options", ["declare-fun", "tickleBool", ["Bool"], "Bool"], ["assert", ["and", ["tickleBool", "true"], ["tickleBool", "false"]]], ["declare-sort", "T@FieldName", "0"], ["declare-sort", "T@String", "0"], ["declare-datatypes", [["T@Edge", "0"]], [[["Field", ["|f#Field|", "T@FieldName"]], ["Index", ["|i#Index|", "Int"]], ["String", ["|s#String|", "T@String"]]]]], ["declare-sort", "T@Address", "0"], ["declare-datatypes", [["T@Value", "0"]], [[["Boolean", ["|b#Boolean|", "Bool"]], ["Integer", ["|i#Integer|", "Int"]], ["Address", ["|a#Address|", "T@Address"]], ["Map", ["|m#Map|", ["Array", "T@Edge", "T@Value"]]]]]], ["declare-datatypes", [["T@ResourceStore", "0"]], [[["ResourceStore", ["|domain#ResourceStore|", ["Array", "T@Address", "Bool"]], ["|contents#ResourceStore|", ["Array", "T@Address", "T@Value"]]]]]], ["declare-datatypes", [["T@Path", "0"]], [[["Nil"], ["Cons", ["|p#Cons|", "T@Path"], ["|e#Cons|", "T@Edge"]]]]], ["declare-sort", "T@TypeName", "0"], ["declare-sort", "T@LocalName", "0"], ["declare-datatypes", [["T@Reference", "0"]], [[["GlobalReference", ["|a#GlobalReference|", "T@Address"], ["|t#GlobalReference|", "T@TypeName"], ["|p#GlobalReference|", "T@Path"], ["|v#GlobalReference|", "T@Value"]], ["LocalReference", ["|c#LocalReference|", "Int"], ["|l#LocalReference|", "T@LocalName"], ["|p#LocalReference|", "T@Path"], ["|v#LocalReference|", "T@Value"]]]]], ["declare-fun", "TestReference_T", [], "T@TypeName"], ["declare-fun", "TestReference_T_value", [], "T@FieldName"], ["declare-fun", "t0_LocalName", [], "T@LocalName"], ["declare-fun", "t1_LocalName", [], "T@LocalName"], ["declare-fun", "t2_LocalName", [], "T@LocalName"], ["declare-fun", "t3_LocalName", [], "T@LocalName"], ["declare-fun", "t4_LocalName", [], "T@LocalName"], ["declare-fun", "t5_LocalName", [], "T@LocalName"], ["declare-fun", "t6_LocalName", [], "T@LocalName"], ["declare-fun", "t7_LocalName", [], "T@LocalName"], ["declare-fun", "t8_LocalName", [], "T@LocalName"], ["declare-fun", "t9_LocalName", [], "T@LocalName"], ["declare-fun", "t10_LocalName", [], "T@LocalName"], ["declare-fun", "t11_LocalName", [], "T@LocalName"], ["declare-fun", "t12_LocalName", [], "T@LocalName"], ["declare-fun", "t13_LocalName", [], "T@LocalName"], ["declare-fun", "t14_LocalName", [], "T@LocalName"], ["declare-fun", "t15_LocalName", [], "T@LocalName"], ["declare-fun", "t16_LocalName", [], "T@LocalName"], ["assert", ["distinct", "t0_LocalName", "t1_LocalName", "t2_LocalName", "t3_LocalName", "t4_LocalName", "t5_LocalName", "t6_LocalName", "t7_LocalName", "t8_LocalName", "t9_LocalName", "t10_LocalName", "t11_LocalName", "t12_LocalName", "t13_LocalName", "t14_LocalName", "t15_LocalName", "t16_LocalName"]], ["declare-fun", "ControlFlow", ["Int", "Int"], "Int"], ["declare-fun", "%lbl%+0", [], "Bool"], ["declare-fun", "%lbl%+1", [], "Bool"], ["declare-fun", "inline$IsPrefix0$1$srcPath@0", [], "T@Path"], ["declare-fun", "%lbl%@2", [], "Bool"], ["declare-fun", "%lbl%+3", [], "Bool"], ["declare-fun", "%lbl%+4", [], "Bool"], ["declare-fun", "inline$IsPrefix0$0$srcPath@0", [], "T@Path"], ["declare-fun", "%lbl%@5", [], "Bool"], ["declare-fun", "%lbl%+6", [], "Bool"], ["declare-fun", "%lbl%+7", [], "Bool"], ["declare-fun", "|inline$UpdateValueMax$2$dstValue'@1|", [], "T@Value"], ["declare-fun", "inline$UpdateValueMax$2$dstValue@0", [], "T@Value"], ["declare-fun", "inline$UpdateValueMax$2$e@0", [], "T@Edge"], ["declare-fun", "inline$UpdateValueMax$2$srcValue@0", [], "T@Value"], ["declare-fun", "%lbl%+8", [], "Bool"], ["declare-fun", "inline$UpdateValueMax$2$srcPath@0", [], "T@Path"], ["declare-fun", "inline$UpdateValue0$2$dstPath@0", [], "T@Path"], ["declare-fun", "%lbl%+9", [], "Bool"], ["declare-fun", "inline$UpdateValueMax$2$dstPath@0", [], "T@Path"], ["declare-fun", "%lbl%+10", [], "Bool"], ["declare-fun", "%lbl%+11", [], "Bool"], ["declare-fun", "inline$UpdateValue0$2$dstValue@0", [], "T@Value"], ["declare-fun", "%lbl%+12", [], "Bool"], ["declare-fun", "%lbl%+13", [], "Bool"], ["declare-fun", "|inline$WriteRef$0$to'@3|", [], "T@Reference"], ["declare-fun", "rs_TestReference_T", [], "T@ResourceStore"], ["declare-fun", "%lbl%+14", [], "Bool"], ["declare-fun", "%lbl%+15", [], "Bool"], ["declare-fun", "%lbl%+16", [], "Bool"], ["declare-fun", "|inline$DeepUpdateReference$0$dst'@2|", [], "T@Reference"], ["declare-fun", "arg0", [], "T@Reference"], ["declare-fun", "|inline$UpdateValueMax$1$dstValue'|", [], "T@Value"], ["declare-fun", "%lbl%+17", [], "Bool"], ["declare-fun", "|inline$UpdateValueMax$1$dstValue'@1|", [], "T@Value"], ["declare-fun", "inline$UpdateValueMax$1$dstValue@0", [], "T@Value"], ["declare-fun", "inline$UpdateValueMax$1$e@0", [], "T@Edge"], ["declare-fun", "inline$UpdateValueMax$1$srcValue@0", [], "T@Value"], ["declare-fun", "%lbl%+18", [], "Bool"], ["declare-fun", "inline$UpdateValueMax$1$srcPath@0", [], "T@Path"], ["declare-fun", "inline$UpdateValue0$1$dstPath@0", [], "T@Path"], ["declare-fun", "%lbl%+19", [], "Bool"], ["declare-fun", "inline$UpdateValueMax$1$dstPath@0", [], "T@Path"], ["declare-fun", "inline$UpdateValue0$1$dstValue@0", [], "T@Value"], ["declare-fun", "%lbl%+20", [], "Bool"], ["declare-fun", "%lbl%+21", [], "Bool"], ["declare-fun", "%lbl%+22", [], "Bool"], ["declare-fun", "%lbl%+23", [], "Bool"], ["declare-fun", "inline$IsPrefixMax$1$isPrefix@1", [], "Bool"], ["declare-fun", "%lbl%+24", [], "Bool"], ["declare-fun", "%lbl%+25", [], "Bool"], ["declare-fun", "inline$IsPrefix0$1$isPrefix@1", [], "Bool"], ["declare-fun", "%lbl%+26", [], "Bool"], ["declare-fun", "%lbl%+27", [], "Bool"], ["declare-fun", "inline$IsPrefixMax$1$dstPath@0", [], "T@Path"], ["declare-fun", "%lbl%+28", [], "Bool"], ["declare-fun", "%lbl%+29", [], "Bool"], ["declare-fun", "inline$IsPrefixMax$1$srcPath@0", [], "T@Path"], ["declare-fun", "%lbl%+30", [], "Bool"], ["declare-fun", "%lbl%+31", [], "Bool"], ["declare-fun", "%lbl%+32", [], "Bool"], ["declare-fun", "%lbl%+33", [], "Bool"], ["declare-fun", "%lbl%+34", [], "Bool"], ["declare-fun", "%lbl%+35", [], "Bool"], ["declare-fun", "%lbl%+36", [], "Bool"], ["declare-fun", "%lbl%+37", [], "Bool"], ["declare-fun", "%lbl%+38", [], "Bool"], ["declare-fun", "|inline$DeepUpdateReference$0$dst'@1|", [], "T@Reference"], ["declare-fun", "|inline$UpdateValueMax$0$dstValue'|", [], "T@Value"], ["declare-fun", "%lbl%+39", [], "Bool"], ["declare-fun", "|inline$UpdateValueMax$0$dstValue'@1|", [], "T@Value"], ["declare-fun", "inline$UpdateValueMax$0$dstValue@0", [], "T@Value"], ["declare-fun", "inline$UpdateValueMax$0$e@0", [], "T@Edge"], ["declare-fun", "inline$UpdateValueMax$0$srcValue@0", [], "T@Value"], ["declare-fun", "%lbl%+40", [], "Bool"], ["declare-fun", "inline$UpdateValueMax$0$srcPath@0", [], "T@Path"], ["declare-fun", "inline$UpdateValue0$0$dstPath@0", [], "T@Path"], ["declare-fun", "%lbl%+41", [], "Bool"], ["declare-fun", "inline$UpdateValueMax$0$dstPath@0", [], "T@Path"], ["declare-fun", "inline$UpdateValue0$0$dstValue@0", [], "T@Value"], ["declare-fun", "%lbl%+42", [], "Bool"], ["declare-fun", "%lbl%+43", [], "Bool"], ["declare-fun", "%lbl%+44", [], "Bool"], ["declare-fun", "%lbl%+45", [], "Bool"], ["declare-fun", "inline$IsPrefixMax$0$isPrefix@1", [], "Bool"], ["declare-fun", "%lbl%+46", [], "Bool"], ["declare-fun", "%lbl%+47", [], "Bool"], ["declare-fun", "inline$IsPrefix0$0$isPrefix@1", [], "Bool"], ["declare-fun", "%lbl%+48", [], "Bool"], ["declare-fun", "%lbl%+49", [], "Bool"], ["declare-fun", "inline$IsPrefixMax$0$dstPath@0", [], "T@Path"], ["declare-fun", "%lbl%+50", [], "Bool"], ["declare-fun", "%lbl%+51", [], "Bool"], ["declare-fun", "inline$IsPrefixMax$0$srcPath@0", [], "T@Path"], ["declare-fun", "%lbl%+52", [], "Bool"], ["declare-fun", "%lbl%+53", [], "Bool"], ["declare-fun", "%lbl%+54", [], "Bool"], ["declare-fun", "%lbl%+55", [], "Bool"], ["declare-fun", "%lbl%+56", [], "Bool"], ["declare-fun", "%lbl%+57", [], "Bool"], ["declare-fun", "%lbl%+58", [], "Bool"], ["declare-fun", "%lbl%+59", [], "Bool"], ["declare-fun", "%lbl%+60", [], "Bool"], ["declare-fun", "|inline$WriteRef$0$to'@2|", [], "T@Reference"], ["declare-fun", "inline$LdConst$0$ret@1", [], "T@Value"], ["declare-fun", "%lbl%+61", [], "Bool"], ["declare-fun", "|inline$WriteRef$0$to'@1|", [], "T@Reference"], ["declare-fun", "%lbl%+62", [], "Bool"], ["declare-fun", "%lbl%+63", [], "Bool"], ["declare-fun", "|c'|", [], "Int"], ["declare-fun", "c", [], "Int"], ["declare-fun", "%lbl%+64", [], "Bool"], ["push", "1"], ["set-info", ":boogie-vc-id", "TestReference_mut_b"], ["assert", ["not", ["=>", ["=", ["ControlFlow", "0", "0"], "16187"], ["let", [["inline$UpdateValue0$1$anon3_Else_correct", ["=>", ["and", "%lbl%+0", "true"], "true"]]], ["let", [["inline$IsPrefix0$1$anon5_Else_correct", ["=>", ["and", "%lbl%+1", "true"], ["=>", ["not", ["=", "inline$IsPrefix0$1$srcPath@0", "Nil"]], ["or", "%lbl%@2", ["=>", ["=", ["ControlFlow", "0", "4205"], ["-", "0", "16915"]], "false"]]]]]], ["let", [["inline$UpdateValue0$0$anon3_Else_correct", ["=>", ["and", "%lbl%+3", "true"], "true"]]], ["let", [["inline$IsPrefix0$0$anon5_Else_correct", ["=>", ["and", "%lbl%+4", "true"], ["=>", ["not", ["=", "inline$IsPrefix0$0$srcPath@0", "Nil"]], ["or", "%lbl%@5", ["=>", ["=", ["ControlFlow", "0", "3647"], ["-", "0", "16619"]], "false"]]]]]], ["let", [["inline$DeepUpdateGlobal$0$anon2_Then$1_correct", ["=>", ["and", "%lbl%+6", "true"], "true"]]], ["let", [["inline$UpdateValueMax$2$anon3_Else$1_correct", ["=>", ["and", "%lbl%+7", "true"], ["=>", ["and", ["=", "|inline$UpdateValueMax$2$dstValue'@1|", ["Map", ["store", ["|m#Map|", "inline$UpdateValueMax$2$dstValue@0"], "inline$UpdateValueMax$2$e@0", "inline$UpdateValueMax$2$srcValue@0"]]], ["=", ["ControlFlow", "0", "4883"], "4919"]], "inline$DeepUpdateGlobal$0$anon2_Then$1_correct"]]]], ["let", [["inline$UpdateValue0$2$anon3_Then_correct", ["=>", ["and", "%lbl%+8", "true"], ["=>", ["and", ["=", "inline$UpdateValueMax$2$srcPath@0", "inline$UpdateValue0$2$dstPath@0"], ["=", ["ControlFlow", "0", "4863"], "4883"]], "inline$UpdateValueMax$2$anon3_Else$1_correct"]]]], ["let", [["inline$UpdateValueMax$2$anon3_Then_correct", ["=>", ["and", "%lbl%+9", "true"], ["=>", ["and", ["=", "inline$UpdateValueMax$2$srcPath@0", "inline$UpdateValueMax$2$dstPath@0"], ["=", ["ControlFlow", "0", "4893"], "4919"]], "inline$DeepUpdateGlobal$0$anon2_Then$1_correct"]]]], ["let", [["inline$UpdateValue0$2$anon3_Else_correct", ["=>", ["and", "%lbl%+10", "true"], "true"]]], ["let", [["inline$UpdateValue0$2$Entry_correct", ["=>", ["and", "%lbl%+11", "true"], ["=>", ["and", ["=", "inline$UpdateValue0$2$dstPath@0", ["Cons", "inline$UpdateValueMax$2$dstPath@0", "inline$UpdateValueMax$2$e@0"]], ["=", "inline$UpdateValue0$2$dstValue@0", ["select", ["|m#Map|", "inline$UpdateValueMax$2$dstValue@0"], "inline$UpdateValueMax$2$e@0"]]], ["and", ["=>", ["=", ["ControlFlow", "0", "4841"], "4863"], "inline$UpdateValue0$2$anon3_Then_correct"], ["=>", ["=", ["ControlFlow", "0", "4841"], "4853"], "inline$UpdateValue0$2$anon3_Else_correct"]]]]]], ["let", [["inline$UpdateValueMax$2$anon3_Else_correct", ["=>", ["and", "%lbl%+12", "true"], ["=>", ["and", ["not", ["=", "inline$UpdateValueMax$2$srcPath@0", "inline$UpdateValueMax$2$dstPath@0"]], ["=", ["ControlFlow", "0", "4869"], "4841"]], "inline$UpdateValue0$2$Entry_correct"]]]], ["let", [["inline$UpdateValueMax$2$Entry_correct", ["=>", ["and", "%lbl%+13", "true"], ["=>", ["and", ["and", ["=", "inline$UpdateValueMax$2$srcPath@0", ["|p#GlobalReference|", "|inline$WriteRef$0$to'@3|"]], ["=", "inline$UpdateValueMax$2$srcValue@0", ["|v#GlobalReference|", "|inline$WriteRef$0$to'@3|"]]], ["and", ["=", "inline$UpdateValueMax$2$dstPath@0", "Nil"], ["=", "inline$UpdateValueMax$2$dstValue@0", ["select", ["|contents#ResourceStore|", "rs_TestReference_T"], ["|a#GlobalReference|", "|inline$WriteRef$0$to'@3|"]]]]], ["and", ["=>", ["=", ["ControlFlow", "0", "4762"], "4893"], "inline$UpdateValueMax$2$anon3_Then_correct"], ["=>", ["=", ["ControlFlow", "0", "4762"], "4869"], "inline$UpdateValueMax$2$anon3_Else_correct"]]]]]], ["let", [["inline$DeepUpdateGlobal$0$anon2_Then_correct", ["=>", ["and", "%lbl%+14", "true"], ["=>", ["and", ["and", ["is-GlobalReference", "|inline$WriteRef$0$to'@3|"], ["=", "TestReference_T", ["|t#GlobalReference|", "|inline$WriteRef$0$to'@3|"]]], ["=", ["ControlFlow", "0", "4899"], "4762"]], "inline$UpdateValueMax$2$Entry_correct"]]]], ["let", [["inline$DeepUpdateGlobal$0$anon2_Else_correct", ["=>", ["and", "%lbl%+15", "true"], "true"]]], ["let", [["inline$DeepUpdateReference$0$anon9_Then$1_correct", ["=>", ["and", "%lbl%+16", "true"], ["=>", ["=", "|inline$DeepUpdateReference$0$dst'@2|", ["LocalReference", ["|c#LocalReference|", "arg0"], ["|l#LocalReference|", "arg0"], ["|p#LocalReference|", "arg0"], "|inline$UpdateValueMax$1$dstValue'|"]], ["and", ["=>", ["=", ["ControlFlow", "0", "4519"], "4899"], "inline$DeepUpdateGlobal$0$anon2_Then_correct"], ["=>", ["=", ["ControlFlow", "0", "4519"], "4649"], "inline$DeepUpdateGlobal$0$anon2_Else_correct"]]]]]], ["let", [["inline$UpdateValueMax$1$anon3_Else$1_correct", ["=>", ["and", "%lbl%+17", "true"], ["=>", ["and", ["=", "|inline$UpdateValueMax$1$dstValue'@1|", ["Map", ["store", ["|m#Map|", "inline$UpdateValueMax$1$dstValue@0"], "inline$UpdateValueMax$1$e@0", "inline$UpdateValueMax$1$srcValue@0"]]], ["=", ["ControlFlow", "0", "4485"], "4519"]], "inline$DeepUpdateReference$0$anon9_Then$1_correct"]]]], ["let", [["inline$UpdateValue0$1$anon3_Then_correct", ["=>", ["and", "%lbl%+18", "true"], ["=>", ["and", ["=", "inline$UpdateValueMax$1$srcPath@0", "inline$UpdateValue0$1$dstPath@0"], ["=", ["ControlFlow", "0", "4465"], "4485"]], "inline$UpdateValueMax$1$anon3_Else$1_correct"]]]], ["let", [["inline$UpdateValue0$1$Entry_correct", ["=>", ["and", "%lbl%+19", "true"], ["=>", ["and", ["=", "inline$UpdateValue0$1$dstPath@0", ["Cons", "inline$UpdateValueMax$1$dstPath@0", "inline$UpdateValueMax$1$e@0"]], ["=", "inline$UpdateValue0$1$dstValue@0", ["select", ["|m#Map|", "inline$UpdateValueMax$1$dstValue@0"], "inline$UpdateValueMax$1$e@0"]]], ["and", ["=>", ["=", ["ControlFlow", "0", "4443"], "4465"], "inline$UpdateValue0$1$anon3_Then_correct"], ["=>", ["=", ["ControlFlow", "0", "4443"], "4455"], "inline$UpdateValue0$1$anon3_Else_correct"]]]]]], ["let", [["inline$UpdateValueMax$1$anon3_Else_correct", ["=>", ["and", "%lbl%+20", "true"], ["=>", ["and", ["not", ["=", "inline$UpdateValueMax$1$srcPath@0", "inline$UpdateValueMax$1$dstPath@0"]], ["=", ["ControlFlow", "0", "4471"], "4443"]], "inline$UpdateValue0$1$Entry_correct"]]]], ["let", [["inline$UpdateValueMax$1$anon3_Then_correct", ["=>", ["and", "%lbl%+21", "true"], ["=>", ["and", ["=", "inline$UpdateValueMax$1$srcPath@0", "inline$UpdateValueMax$1$dstPath@0"], ["=", ["ControlFlow", "0", "4495"], "4519"]], "inline$DeepUpdateReference$0$anon9_Then$1_correct"]]]], ["let", [["inline$UpdateValueMax$1$Entry_correct", ["=>", ["and", "%lbl%+22", "true"], ["=>", ["and", ["and", ["=", "inline$UpdateValueMax$1$srcPath@0", ["|p#LocalReference|", "|inline$WriteRef$0$to'@3|"]], ["=", "inline$UpdateValueMax$1$srcValue@0", ["|v#LocalReference|", "|inline$WriteRef$0$to'@3|"]]], ["and", ["=", "inline$UpdateValueMax$1$dstPath@0", ["|p#LocalReference|", "arg0"]], ["=", "inline$UpdateValueMax$1$dstValue@0", ["|v#LocalReference|", "arg0"]]]], ["and", ["=>", ["=", ["ControlFlow", "0", "4364"], "4495"], "inline$UpdateValueMax$1$anon3_Then_correct"], ["=>", ["=", ["ControlFlow", "0", "4364"], "4471"], "inline$UpdateValueMax$1$anon3_Else_correct"]]]]]], ["let", [["inline$DeepUpdateReference$0$anon9_Then_correct", ["=>", ["and", "%lbl%+23", "true"], ["=>", ["and", "inline$IsPrefixMax$1$isPrefix@1", ["=", ["ControlFlow", "0", "4501"], "4364"]], "inline$UpdateValueMax$1$Entry_correct"]]]], ["let", [["inline$DeepUpdateReference$0$anon9_Else_correct", ["=>", ["and", "%lbl%+24", "true"], ["=>", ["not", "inline$IsPrefixMax$1$isPrefix@1"], ["and", ["=>", ["=", ["ControlFlow", "0", "4267"], "4899"], "inline$DeepUpdateGlobal$0$anon2_Then_correct"], ["=>", ["=", ["ControlFlow", "0", "4267"], "4649"], "inline$DeepUpdateGlobal$0$anon2_Else_correct"]]]]]], ["let", [["inline$IsPrefixMax$1$anon5_Else$1_correct", ["=>", ["and", "%lbl%+25", "true"], ["=>", ["and", ["=>", "inline$IsPrefixMax$1$isPrefix@1", "inline$IsPrefix0$1$isPrefix@1"], ["=>", "inline$IsPrefix0$1$isPrefix@1", "inline$IsPrefixMax$1$isPrefix@1"]], ["and", ["=>", ["=", ["ControlFlow", "0", "4233"], "4501"], "inline$DeepUpdateReference$0$anon9_Then_correct"], ["=>", ["=", ["ControlFlow", "0", "4233"], "4267"], "inline$DeepUpdateReference$0$anon9_Else_correct"]]]]]], ["let", [["inline$IsPrefix0$1$anon5_Then_correct", ["=>", ["and", "%lbl%+26", "true"], ["=>", ["=", "inline$IsPrefix0$1$srcPath@0", "Nil"], ["=>", ["and", ["and", ["=>", "inline$IsPrefix0$1$isPrefix@1", "false"], ["=>", "false", "inline$IsPrefix0$1$isPrefix@1"]], ["=", ["ControlFlow", "0", "4215"], "4233"]], "inline$IsPrefixMax$1$anon5_Else$1_correct"]]]]], ["let", [["inline$IsPrefix0$1$anon4_Else_correct", ["=>", ["and", "%lbl%+27", "true"], ["=>", ["not", ["=", "inline$IsPrefix0$1$srcPath@0", "inline$IsPrefixMax$1$dstPath@0"]], ["and", ["=>", ["=", ["ControlFlow", "0", "4195"], "4215"], "inline$IsPrefix0$1$anon5_Then_correct"], ["=>", ["=", ["ControlFlow", "0", "4195"], "4205"], "inline$IsPrefix0$1$anon5_Else_correct"]]]]]], ["let", [["inline$IsPrefix0$1$anon4_Then_correct", ["=>", ["and", "%lbl%+28", "true"], ["=>", ["=", "inline$IsPrefix0$1$srcPath@0", "inline$IsPrefixMax$1$dstPath@0"], ["=>", ["and", ["and", ["=>", "inline$IsPrefix0$1$isPrefix@1", "true"], ["=>", "true", "inline$IsPrefix0$1$isPrefix@1"]], ["=", ["ControlFlow", "0", "4225"], "4233"]], "inline$IsPrefixMax$1$anon5_Else$1_correct"]]]]], ["let", [["inline$IsPrefix0$1$Entry_correct", ["=>", ["and", "%lbl%+29", "true"], ["=>", ["=", "inline$IsPrefix0$1$srcPath@0", ["|p#Cons|", "inline$IsPrefixMax$1$srcPath@0"]], ["and", ["=>", ["=", ["ControlFlow", "0", "4185"], "4225"], "inline$IsPrefix0$1$anon4_Then_correct"], ["=>", ["=", ["ControlFlow", "0", "4185"], "4195"], "inline$IsPrefix0$1$anon4_Else_correct"]]]]]], ["let", [["inline$IsPrefixMax$1$anon5_Else_correct", ["=>", ["and", "%lbl%+30", "true"], ["=>", ["and", ["not", ["=", "inline$IsPrefixMax$1$srcPath@0", "Nil"]], ["=", ["ControlFlow", "0", "4231"], "4185"]], "inline$IsPrefix0$1$Entry_correct"]]]], ["let", [["inline$IsPrefixMax$1$anon5_Then_correct", ["=>", ["and", "%lbl%+31", "true"], ["=>", ["=", "inline$IsPrefixMax$1$srcPath@0", "Nil"], ["=>", ["and", ["=>", "inline$IsPrefixMax$1$isPrefix@1", "false"], ["=>", "false", "inline$IsPrefixMax$1$isPrefix@1"]], ["and", ["=>", ["=", ["ControlFlow", "0", "4243"], "4501"], "inline$DeepUpdateReference$0$anon9_Then_correct"], ["=>", ["=", ["ControlFlow", "0", "4243"], "4267"], "inline$DeepUpdateReference$0$anon9_Else_correct"]]]]]]], ["let", [["inline$IsPrefixMax$1$anon4_Else_correct", ["=>", ["and", "%lbl%+32", "true"], ["=>", ["not", ["=", "inline$IsPrefixMax$1$srcPath@0", "inline$IsPrefixMax$1$dstPath@0"]], ["and", ["=>", ["=", ["ControlFlow", "0", "4110"], "4243"], "inline$IsPrefixMax$1$anon5_Then_correct"], ["=>", ["=", ["ControlFlow", "0", "4110"], "4231"], "inline$IsPrefixMax$1$anon5_Else_correct"]]]]]], ["let", [["inline$IsPrefixMax$1$anon4_Then_correct", ["=>", ["and", "%lbl%+33", "true"], ["=>", ["=", "inline$IsPrefixMax$1$srcPath@0", "inline$IsPrefixMax$1$dstPath@0"], ["=>", ["and", ["=>", "inline$IsPrefixMax$1$isPrefix@1", "true"], ["=>", "true", "inline$IsPrefixMax$1$isPrefix@1"]], ["and", ["=>", ["=", ["ControlFlow", "0", "4253"], "4501"], "inline$DeepUpdateReference$0$anon9_Then_correct"], ["=>", ["=", ["ControlFlow", "0", "4253"], "4267"], "inline$DeepUpdateReference$0$anon9_Else_correct"]]]]]]], ["let", [["inline$IsPrefixMax$1$Entry_correct", ["=>", ["and", "%lbl%+34", "true"], ["=>", ["and", ["=", "inline$IsPrefixMax$1$dstPath@0", ["|p#LocalReference|", "arg0"]], ["=", "inline$IsPrefixMax$1$srcPath@0", ["|p#LocalReference|", "|inline$WriteRef$0$to'@3|"]]], ["and", ["=>", ["=", ["ControlFlow", "0", "4100"], "4253"], "inline$IsPrefixMax$1$anon4_Then_correct"], ["=>", ["=", ["ControlFlow", "0", "4100"], "4110"], "inline$IsPrefixMax$1$anon4_Else_correct"]]]]]], ["let", [["inline$DeepUpdateReference$0$anon8_Then_correct", ["=>", ["and", "%lbl%+35", "true"], ["=>", ["and", ["and", ["and", ["is-LocalReference", "arg0"], ["=", ["|c#LocalReference|", "|inline$WriteRef$0$to'@3|"], ["|c#LocalReference|", "arg0"]]], ["=", ["|l#LocalReference|", "|inline$WriteRef$0$to'@3|"], ["|l#LocalReference|", "arg0"]]], ["=", ["ControlFlow", "0", "4259"], "4100"]], "inline$IsPrefixMax$1$Entry_correct"]]]], ["let", [["inline$DeepUpdateReference$0$anon8_Else_correct", ["=>", ["and", "%lbl%+36", "true"], ["=>", ["not", ["and", ["and", ["is-LocalReference", "arg0"], ["=", ["|c#LocalReference|", "|inline$WriteRef$0$to'@3|"], ["|c#LocalReference|", "arg0"]]], ["=", ["|l#LocalReference|", "|inline$WriteRef$0$to'@3|"], ["|l#LocalReference|", "arg0"]]]], ["and", ["=>", ["=", ["ControlFlow", "0", "3999"], "4899"], "inline$DeepUpdateGlobal$0$anon2_Then_correct"], ["=>", ["=", ["ControlFlow", "0", "3999"], "4649"], "inline$DeepUpdateGlobal$0$anon2_Else_correct"]]]]]], ["let", [["inline$DeepUpdateReference$0$anon7_Then_correct", ["=>", ["and", "%lbl%+37", "true"], ["=>", ["is-LocalReference", "|inline$WriteRef$0$to'@3|"], ["and", ["=>", ["=", ["ControlFlow", "0", "3967"], "4259"], "inline$DeepUpdateReference$0$anon8_Then_correct"], ["=>", ["=", ["ControlFlow", "0", "3967"], "3999"], "inline$DeepUpdateReference$0$anon8_Else_correct"]]]]]], ["let", [["inline$DeepUpdateReference$0$anon11_Then$1_correct", ["=>", ["and", "%lbl%+38", "true"], ["=>", ["=", "|inline$DeepUpdateReference$0$dst'@1|", ["GlobalReference", ["|a#GlobalReference|", "arg0"], ["|t#GlobalReference|", "arg0"], ["|p#GlobalReference|", "arg0"], "|inline$UpdateValueMax$0$dstValue'|"]], ["and", ["=>", ["=", ["ControlFlow", "0", "3961"], "4899"], "inline$DeepUpdateGlobal$0$anon2_Then_correct"], ["=>", ["=", ["ControlFlow", "0", "3961"], "4649"], "inline$DeepUpdateGlobal$0$anon2_Else_correct"]]]]]], ["let", [["inline$UpdateValueMax$0$anon3_Else$1_correct", ["=>", ["and", "%lbl%+39", "true"], ["=>", ["and", ["=", "|inline$UpdateValueMax$0$dstValue'@1|", ["Map", ["store", ["|m#Map|", "inline$UpdateValueMax$0$dstValue@0"], "inline$UpdateValueMax$0$e@0", "inline$UpdateValueMax$0$srcValue@0"]]], ["=", ["ControlFlow", "0", "3927"], "3961"]], "inline$DeepUpdateReference$0$anon11_Then$1_correct"]]]], ["let", [["inline$UpdateValue0$0$anon3_Then_correct", ["=>", ["and", "%lbl%+40", "true"], ["=>", ["and", ["=", "inline$UpdateValueMax$0$srcPath@0", "inline$UpdateValue0$0$dstPath@0"], ["=", ["ControlFlow", "0", "3907"], "3927"]], "inline$UpdateValueMax$0$anon3_Else$1_correct"]]]], ["let", [["inline$UpdateValue0$0$Entry_correct", ["=>", ["and", "%lbl%+41", "true"], ["=>", ["and", ["=", "inline$UpdateValue0$0$dstPath@0", ["Cons", "inline$UpdateValueMax$0$dstPath@0", "inline$UpdateValueMax$0$e@0"]], ["=", "inline$UpdateValue0$0$dstValue@0", ["select", ["|m#Map|", "inline$UpdateValueMax$0$dstValue@0"], "inline$UpdateValueMax$0$e@0"]]], ["and", ["=>", ["=", ["ControlFlow", "0", "3885"], "3907"], "inline$UpdateValue0$0$anon3_Then_correct"], ["=>", ["=", ["ControlFlow", "0", "3885"], "3897"], "inline$UpdateValue0$0$anon3_Else_correct"]]]]]], ["let", [["inline$UpdateValueMax$0$anon3_Else_correct", ["=>", ["and", "%lbl%+42", "true"], ["=>", ["and", ["not", ["=", "inline$UpdateValueMax$0$srcPath@0", "inline$UpdateValueMax$0$dstPath@0"]], ["=", ["ControlFlow", "0", "3913"], "3885"]], "inline$UpdateValue0$0$Entry_correct"]]]], ["let", [["inline$UpdateValueMax$0$anon3_Then_correct", ["=>", ["and", "%lbl%+43", "true"], ["=>", ["and", ["=", "inline$UpdateValueMax$0$srcPath@0", "inline$UpdateValueMax$0$dstPath@0"], ["=", ["ControlFlow", "0", "3937"], "3961"]], "inline$DeepUpdateReference$0$anon11_Then$1_correct"]]]], ["let", [["inline$UpdateValueMax$0$Entry_correct", ["=>", ["and", "%lbl%+44", "true"], ["=>", ["and", ["and", ["=", "inline$UpdateValueMax$0$srcPath@0", ["|p#GlobalReference|", "|inline$WriteRef$0$to'@3|"]], ["=", "inline$UpdateValueMax$0$srcValue@0", ["|v#GlobalReference|", "|inline$WriteRef$0$to'@3|"]]], ["and", ["=", "inline$UpdateValueMax$0$dstPath@0", ["|p#GlobalReference|", "arg0"]], ["=", "inline$UpdateValueMax$0$dstValue@0", ["|v#GlobalReference|", "arg0"]]]], ["and", ["=>", ["=", ["ControlFlow", "0", "3806"], "3937"], "inline$UpdateValueMax$0$anon3_Then_correct"], ["=>", ["=", ["ControlFlow", "0", "3806"], "3913"], "inline$UpdateValueMax$0$anon3_Else_correct"]]]]]], ["let", [["inline$DeepUpdateReference$0$anon11_Then_correct", ["=>", ["and", "%lbl%+45", "true"], ["=>", ["and", "inline$IsPrefixMax$0$isPrefix@1", ["=", ["ControlFlow", "0", "3943"], "3806"]], "inline$UpdateValueMax$0$Entry_correct"]]]], ["let", [["inline$DeepUpdateReference$0$anon11_Else_correct", ["=>", ["and", "%lbl%+46", "true"], ["=>", ["not", "inline$IsPrefixMax$0$isPrefix@1"], ["and", ["=>", ["=", ["ControlFlow", "0", "3709"], "4899"], "inline$DeepUpdateGlobal$0$anon2_Then_correct"], ["=>", ["=", ["ControlFlow", "0", "3709"], "4649"], "inline$DeepUpdateGlobal$0$anon2_Else_correct"]]]]]], ["let", [["inline$IsPrefixMax$0$anon5_Else$1_correct", ["=>", ["and", "%lbl%+47", "true"], ["=>", ["and", ["=>", "inline$IsPrefixMax$0$isPrefix@1", "inline$IsPrefix0$0$isPrefix@1"], ["=>", "inline$IsPrefix0$0$isPrefix@1", "inline$IsPrefixMax$0$isPrefix@1"]], ["and", ["=>", ["=", ["ControlFlow", "0", "3675"], "3943"], "inline$DeepUpdateReference$0$anon11_Then_correct"], ["=>", ["=", ["ControlFlow", "0", "3675"], "3709"], "inline$DeepUpdateReference$0$anon11_Else_correct"]]]]]], ["let", [["inline$IsPrefix0$0$anon5_Then_correct", ["=>", ["and", "%lbl%+48", "true"], ["=>", ["=", "inline$IsPrefix0$0$srcPath@0", "Nil"], ["=>", ["and", ["and", ["=>", "inline$IsPrefix0$0$isPrefix@1", "false"], ["=>", "false", "inline$IsPrefix0$0$isPrefix@1"]], ["=", ["ControlFlow", "0", "3657"], "3675"]], "inline$IsPrefixMax$0$anon5_Else$1_correct"]]]]], ["let", [["inline$IsPrefix0$0$anon4_Else_correct", ["=>", ["and", "%lbl%+49", "true"], ["=>", ["not", ["=", "inline$IsPrefix0$0$srcPath@0", "inline$IsPrefixMax$0$dstPath@0"]], ["and", ["=>", ["=", ["ControlFlow", "0", "3637"], "3657"], "inline$IsPrefix0$0$anon5_Then_correct"], ["=>", ["=", ["ControlFlow", "0", "3637"], "3647"], "inline$IsPrefix0$0$anon5_Else_correct"]]]]]], ["let", [["inline$IsPrefix0$0$anon4_Then_correct", ["=>", ["and", "%lbl%+50", "true"], ["=>", ["=", "inline$IsPrefix0$0$srcPath@0", "inline$IsPrefixMax$0$dstPath@0"], ["=>", ["and", ["and", ["=>", "inline$IsPrefix0$0$isPrefix@1", "true"], ["=>", "true", "inline$IsPrefix0$0$isPrefix@1"]], ["=", ["ControlFlow", "0", "3667"], "3675"]], "inline$IsPrefixMax$0$anon5_Else$1_correct"]]]]], ["let", [["inline$IsPrefix0$0$Entry_correct", ["=>", ["and", "%lbl%+51", "true"], ["=>", ["=", "inline$IsPrefix0$0$srcPath@0", ["|p#Cons|", "inline$IsPrefixMax$0$srcPath@0"]], ["and", ["=>", ["=", ["ControlFlow", "0", "3627"], "3667"], "inline$IsPrefix0$0$anon4_Then_correct"], ["=>", ["=", ["ControlFlow", "0", "3627"], "3637"], "inline$IsPrefix0$0$anon4_Else_correct"]]]]]], ["let", [["inline$IsPrefixMax$0$anon5_Else_correct", ["=>", ["and", "%lbl%+52", "true"], ["=>", ["and", ["not", ["=", "inline$IsPrefixMax$0$srcPath@0", "Nil"]], ["=", ["ControlFlow", "0", "3673"], "3627"]], "inline$IsPrefix0$0$Entry_correct"]]]], ["let", [["inline$IsPrefixMax$0$anon5_Then_correct", ["=>", ["and", "%lbl%+53", "true"], ["=>", ["=", "inline$IsPrefixMax$0$srcPath@0", "Nil"], ["=>", ["and", ["=>", "inline$IsPrefixMax$0$isPrefix@1", "false"], ["=>", "false", "inline$IsPrefixMax$0$isPrefix@1"]], ["and", ["=>", ["=", ["ControlFlow", "0", "3685"], "3943"], "inline$DeepUpdateReference$0$anon11_Then_correct"], ["=>", ["=", ["ControlFlow", "0", "3685"], "3709"], "inline$DeepUpdateReference$0$anon11_Else_correct"]]]]]]], ["let", [["inline$IsPrefixMax$0$anon4_Else_correct", ["=>", ["and", "%lbl%+54", "true"], ["=>", ["not", ["=", "inline$IsPrefixMax$0$srcPath@0", "inline$IsPrefixMax$0$dstPath@0"]], ["and", ["=>", ["=", ["ControlFlow", "0", "3552"], "3685"], "inline$IsPrefixMax$0$anon5_Then_correct"], ["=>", ["=", ["ControlFlow", "0", "3552"], "3673"], "inline$IsPrefixMax$0$anon5_Else_correct"]]]]]], ["let", [["inline$IsPrefixMax$0$anon4_Then_correct", ["=>", ["and", "%lbl%+55", "true"], ["=>", ["=", "inline$IsPrefixMax$0$srcPath@0", "inline$IsPrefixMax$0$dstPath@0"], ["=>", ["and", ["=>", "inline$IsPrefixMax$0$isPrefix@1", "true"], ["=>", "true", "inline$IsPrefixMax$0$isPrefix@1"]], ["and", ["=>", ["=", ["ControlFlow", "0", "3695"], "3943"], "inline$DeepUpdateReference$0$anon11_Then_correct"], ["=>", ["=", ["ControlFlow", "0", "3695"], "3709"], "inline$DeepUpdateReference$0$anon11_Else_correct"]]]]]]], ["let", [["inline$IsPrefixMax$0$Entry_correct", ["=>", ["and", "%lbl%+56", "true"], ["=>", ["and", ["=", "inline$IsPrefixMax$0$dstPath@0", ["|p#GlobalReference|", "arg0"]], ["=", "inline$IsPrefixMax$0$srcPath@0", ["|p#GlobalReference|", "|inline$WriteRef$0$to'@3|"]]], ["and", ["=>", ["=", ["ControlFlow", "0", "3542"], "3695"], "inline$IsPrefixMax$0$anon4_Then_correct"], ["=>", ["=", ["ControlFlow", "0", "3542"], "3552"], "inline$IsPrefixMax$0$anon4_Else_correct"]]]]]], ["let", [["inline$DeepUpdateReference$0$anon10_Then_correct", ["=>", ["and", "%lbl%+57", "true"], ["=>", ["and", ["and", ["and", ["is-GlobalReference", "arg0"], ["=", ["|a#GlobalReference|", "|inline$WriteRef$0$to'@3|"], ["|a#GlobalReference|", "arg0"]]], ["=", ["|t#GlobalReference|", "|inline$WriteRef$0$to'@3|"], ["|t#GlobalReference|", "arg0"]]], ["=", ["ControlFlow", "0", "3701"], "3542"]], "inline$IsPrefixMax$0$Entry_correct"]]]], ["let", [["inline$DeepUpdateReference$0$anon10_Else_correct", ["=>", ["and", "%lbl%+58", "true"], ["=>", ["not", ["and", ["and", ["is-GlobalReference", "arg0"], ["=", ["|a#GlobalReference|", "|inline$WriteRef$0$to'@3|"], ["|a#GlobalReference|", "arg0"]]], ["=", ["|t#GlobalReference|", "|inline$WriteRef$0$to'@3|"], ["|t#GlobalReference|", "arg0"]]]], ["and", ["=>", ["=", ["ControlFlow", "0", "3441"], "4899"], "inline$DeepUpdateGlobal$0$anon2_Then_correct"], ["=>", ["=", ["ControlFlow", "0", "3441"], "4649"], "inline$DeepUpdateGlobal$0$anon2_Else_correct"]]]]]], ["let", [["inline$DeepUpdateReference$0$anon7_Else_correct", ["=>", ["and", "%lbl%+59", "true"], ["=>", ["not", ["is-LocalReference", "|inline$WriteRef$0$to'@3|"]], ["and", ["=>", ["=", ["ControlFlow", "0", "3409"], "3701"], "inline$DeepUpdateReference$0$anon10_Then_correct"], ["=>", ["=", ["ControlFlow", "0", "3409"], "3441"], "inline$DeepUpdateReference$0$anon10_Else_correct"]]]]]], ["let", [["inline$WriteRef$0$anon3_Else_correct", ["=>", ["and", "%lbl%+60", "true"], ["=>", ["not", ["is-GlobalReference", "arg0"]], ["=>", ["and", ["=", "|inline$WriteRef$0$to'@2|", ["LocalReference", ["|c#LocalReference|", "arg0"], ["|l#LocalReference|", "arg0"], ["|p#LocalReference|", "arg0"], "inline$LdConst$0$ret@1"]], ["=", "|inline$WriteRef$0$to'@3|", "|inline$WriteRef$0$to'@2|"]], ["and", ["=>", ["=", ["ControlFlow", "0", "3125"], "3967"], "inline$DeepUpdateReference$0$anon7_Then_correct"], ["=>", ["=", ["ControlFlow", "0", "3125"], "3409"], "inline$DeepUpdateReference$0$anon7_Else_correct"]]]]]]], ["let", [["inline$WriteRef$0$anon3_Then_correct", ["=>", ["and", "%lbl%+61", "true"], ["=>", ["is-GlobalReference", "arg0"], ["=>", ["and", ["=", "|inline$WriteRef$0$to'@1|", ["GlobalReference", ["|a#GlobalReference|", "arg0"], ["|t#GlobalReference|", "arg0"], ["|p#GlobalReference|", "arg0"], "inline$LdConst$0$ret@1"]], ["=", "|inline$WriteRef$0$to'@3|", "|inline$WriteRef$0$to'@1|"]], ["and", ["=>", ["=", ["ControlFlow", "0", "3147"], "3967"], "inline$DeepUpdateReference$0$anon7_Then_correct"], ["=>", ["=", ["ControlFlow", "0", "3147"], "3409"], "inline$DeepUpdateReference$0$anon7_Else_correct"]]]]]]], ["let", [["inline$LdConst$0$anon0_correct", ["=>", ["and", "%lbl%+62", "true"], ["=>", ["=", "inline$LdConst$0$ret@1", ["Integer", "0"]], ["and", ["=>", ["=", ["ControlFlow", "0", "2992"], "3147"], "inline$WriteRef$0$anon3_Then_correct"], ["=>", ["=", ["ControlFlow", "0", "2992"], "3125"], "inline$WriteRef$0$anon3_Else_correct"]]]]]], ["let", [["anon0_correct", ["=>", ["and", "%lbl%+63", "true"], ["=>", ["and", [">", "|c'|", "c"], ["=", ["ControlFlow", "0", "2998"], "2992"]], "inline$LdConst$0$anon0_correct"]]]], ["let", [["PreconditionGeneratedEntry_correct", ["=>", ["and", "%lbl%+64", "true"], ["=>", ["=", ["ControlFlow", "0", "16187"], "2998"], "anon0_correct"]]]], "PreconditionGeneratedEntry_correct"]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]], ["check-sat"], ["set-option", ":print-success", "false"], ["set-info", ":smt-lib-version", "2.0"], ["set-option", ":produce-models", "true"], ["set-option", ":AUTO_CONFIG", "false"], ["set-option", ":pp.bv_literals", "false"], ["set-option", ":MODEL.V2", "true"], ["set-option", ":smt.PHASE_SELECTION", "0"], ["set-option", ":smt.RESTART_STRATEGY", "0"], ["set-option", ":smt.RESTART_FACTOR", "|1.5|"], ["set-option", ":smt.ARITH.RANDOM_INITIAL_VALUE", "true"], ["set-option", ":smt.CASE_SPLIT", "3"], ["set-option", ":smt.DELAY_UNITS", "true"], ["set-option", ":NNF.SK_HACK", "true"], ["set-option", ":smt.MBQI", "false"], ["set-option", ":smt.QI.EAGER_THRESHOLD", "100"], ["set-option", ":TYPE_CHECK", "true"], ["set-option", ":smt.BV.REFLECT", "true"], ["set-option", ":model_compress", "false"], "; done setting options", ["declare-fun", "tickleBool", ["Bool"], "Bool"], ["assert", ["and", ["tickleBool", "true"], ["tickleBool", "false"]]], ["declare-sort", "T@FieldName", "0"], ["declare-sort", "T@String", "0"], ["declare-datatypes", [["T@Edge", "0"]], [[["Field", ["|f#Field|", "T@FieldName"]], ["Index", ["|i#Index|", "Int"]], ["String", ["|s#String|", "T@String"]]]]], ["declare-sort", "T@Address", "0"], ["declare-datatypes", [["T@Value", "0"]], [[["Boolean", ["|b#Boolean|", "Bool"]], ["Integer", ["|i#Integer|", "Int"]], ["Address", ["|a#Address|", "T@Address"]], ["Map", ["|m#Map|", ["Array", "T@Edge", "T@Value"]]]]]], ["declare-datatypes", [["T@ResourceStore", "0"]], [[["ResourceStore", ["|domain#ResourceStore|", ["Array", "T@Address", "Bool"]], ["|contents#ResourceStore|", ["Array", "T@Address", "T@Value"]]]]]], ["declare-datatypes", [["T@Path", "0"]], [[["Nil"], ["Cons", ["|p#Cons|", "T@Path"], ["|e#Cons|", "T@Edge"]]]]], ["declare-sort", "T@TypeName", "0"], ["declare-sort", "T@LocalName", "0"], ["declare-datatypes", [["T@Reference", "0"]], [[["GlobalReference", ["|a#GlobalReference|", "T@Address"], ["|t#GlobalReference|", "T@TypeName"], ["|p#GlobalReference|", "T@Path"], ["|v#GlobalReference|", "T@Value"]], ["LocalReference", ["|c#LocalReference|", "Int"], ["|l#LocalReference|", "T@LocalName"], ["|p#LocalReference|", "T@Path"], ["|v#LocalReference|", "T@Value"]]]]], ["declare-fun", "TestReference_T", [], "T@TypeName"], ["declare-fun", "TestReference_T_value", [], "T@FieldName"], ["declare-fun", "t0_LocalName", [], "T@LocalName"], ["declare-fun", "t1_LocalName", [], "T@LocalName"], ["declare-fun", "t2_LocalName", [], "T@LocalName"], ["declare-fun", "t3_LocalName", [], "T@LocalName"], ["declare-fun", "t4_LocalName", [], "T@LocalName"], ["declare-fun", "t5_LocalName", [], "T@LocalName"], ["declare-fun", "t6_LocalName", [], "T@LocalName"], ["declare-fun", "t7_LocalName", [], "T@LocalName"], ["declare-fun", "t8_LocalName", [], "T@LocalName"], ["declare-fun", "t9_LocalName", [], "T@LocalName"], ["declare-fun", "t10_LocalName", [], "T@LocalName"], ["declare-fun", "t11_LocalName", [], "T@LocalName"], ["declare-fun", "t12_LocalName", [], "T@LocalName"], ["declare-fun", "t13_LocalName", [], "T@LocalName"], ["declare-fun", "t14_LocalName", [], "T@LocalName"], ["declare-fun", "t15_LocalName", [], "T@LocalName"], ["declare-fun", "t16_LocalName", [], "T@LocalName"], ["assert", ["distinct", "t0_LocalName", "t1_LocalName", "t2_LocalName", "t3_LocalName", "t4_LocalName", "t5_LocalName", "t6_LocalName", "t7_LocalName", "t8_LocalName", "t9_LocalName", "t10_LocalName", "t11_LocalName", "t12_LocalName", "t13_LocalName", "t14_LocalName", "t15_LocalName", "t16_LocalName"]], ["declare-fun", "ControlFlow", ["Int", "Int"], "Int"], ["declare-fun", "%lbl%+0", [], "Bool"], ["declare-fun", "%lbl%+1", [], "Bool"], ["declare-fun", "inline$IsPrefix0$1$srcPath@0", [], "T@Path"], ["declare-fun", "%lbl%@2", [], "Bool"], ["declare-fun", "%lbl%+3", [], "Bool"], ["declare-fun", "%lbl%+4", [], "Bool"], ["declare-fun", "inline$IsPrefix0$0$srcPath@0", [], "T@Path"], ["declare-fun", "%lbl%@5", [], "Bool"], ["declare-fun", "%lbl%+6", [], "Bool"], ["declare-fun", "%lbl%+7", [], "Bool"], ["declare-fun", "|inline$UpdateValueMax$2$dstValue'@1|", [], "T@Value"], ["declare-fun", "inline$UpdateValueMax$2$dstValue@0", [], "T@Value"], ["declare-fun", "inline$UpdateValueMax$2$e@0", [], "T@Edge"], ["declare-fun", "inline$UpdateValueMax$2$srcValue@0", [], "T@Value"], ["declare-fun", "%lbl%+8", [], "Bool"], ["declare-fun", "inline$UpdateValueMax$2$srcPath@0", [], "T@Path"], ["declare-fun", "inline$UpdateValue0$2$dstPath@0", [], "T@Path"], ["declare-fun", "%lbl%+9", [], "Bool"], ["declare-fun", "inline$UpdateValueMax$2$dstPath@0", [], "T@Path"], ["declare-fun", "%lbl%+10", [], "Bool"], ["declare-fun", "%lbl%+11", [], "Bool"], ["declare-fun", "inline$UpdateValue0$2$dstValue@0", [], "T@Value"], ["declare-fun", "%lbl%+12", [], "Bool"], ["declare-fun", "%lbl%+13", [], "Bool"], ["declare-fun", "|inline$WriteRef$0$to'@3|", [], "T@Reference"], ["declare-fun", "rs_TestReference_T", [], "T@ResourceStore"], ["declare-fun", "%lbl%+14", [], "Bool"], ["declare-fun", "%lbl%+15", [], "Bool"], ["declare-fun", "%lbl%+16", [], "Bool"], ["declare-fun", "|inline$DeepUpdateReference$0$dst'@2|", [], "T@Reference"], ["declare-fun", "arg0", [], "T@Reference"], ["declare-fun", "|inline$UpdateValueMax$1$dstValue'|", [], "T@Value"], ["declare-fun", "%lbl%+17", [], "Bool"], ["declare-fun", "|inline$UpdateValueMax$1$dstValue'@1|", [], "T@Value"], ["declare-fun", "inline$UpdateValueMax$1$dstValue@0", [], "T@Value"], ["declare-fun", "inline$UpdateValueMax$1$e@0", [], "T@Edge"], ["declare-fun", "inline$UpdateValueMax$1$srcValue@0", [], "T@Value"], ["declare-fun", "%lbl%+18", [], "Bool"], ["declare-fun", "inline$UpdateValueMax$1$srcPath@0", [], "T@Path"], ["declare-fun", "inline$UpdateValue0$1$dstPath@0", [], "T@Path"], ["declare-fun", "%lbl%+19", [], "Bool"], ["declare-fun", "inline$UpdateValueMax$1$dstPath@0", [], "T@Path"], ["declare-fun", "inline$UpdateValue0$1$dstValue@0", [], "T@Value"], ["declare-fun", "%lbl%+20", [], "Bool"], ["declare-fun", "%lbl%+21", [], "Bool"], ["declare-fun", "%lbl%+22", [], "Bool"], ["declare-fun", "%lbl%+23", [], "Bool"], ["declare-fun", "inline$IsPrefixMax$1$isPrefix@1", [], "Bool"], ["declare-fun", "%lbl%+24", [], "Bool"], ["declare-fun", "%lbl%+25", [], "Bool"], ["declare-fun", "inline$IsPrefix0$1$isPrefix@1", [], "Bool"], ["declare-fun", "%lbl%+26", [], "Bool"], ["declare-fun", "%lbl%+27", [], "Bool"], ["declare-fun", "inline$IsPrefixMax$1$dstPath@0", [], "T@Path"], ["declare-fun", "%lbl%+28", [], "Bool"], ["declare-fun", "%lbl%+29", [], "Bool"], ["declare-fun", "inline$IsPrefixMax$1$srcPath@0", [], "T@Path"], ["declare-fun", "%lbl%+30", [], "Bool"], ["declare-fun", "%lbl%+31", [], "Bool"], ["declare-fun", "%lbl%+32", [], "Bool"], ["declare-fun", "%lbl%+33", [], "Bool"], ["declare-fun", "%lbl%+34", [], "Bool"], ["declare-fun", "%lbl%+35", [], "Bool"], ["declare-fun", "%lbl%+36", [], "Bool"], ["declare-fun", "%lbl%+37", [], "Bool"], ["declare-fun", "%lbl%+38", [], "Bool"], ["declare-fun", "|inline$DeepUpdateReference$0$dst'@1|", [], "T@Reference"], ["declare-fun", "|inline$UpdateValueMax$0$dstValue'|", [], "T@Value"], ["declare-fun", "%lbl%+39", [], "Bool"], ["declare-fun", "|inline$UpdateValueMax$0$dstValue'@1|", [], "T@Value"], ["declare-fun", "inline$UpdateValueMax$0$dstValue@0", [], "T@Value"], ["declare-fun", "inline$UpdateValueMax$0$e@0", [], "T@Edge"], ["declare-fun", "inline$UpdateValueMax$0$srcValue@0", [], "T@Value"], ["declare-fun", "%lbl%+40", [], "Bool"], ["declare-fun", "inline$UpdateValueMax$0$srcPath@0", [], "T@Path"], ["declare-fun", "inline$UpdateValue0$0$dstPath@0", [], "T@Path"], ["declare-fun", "%lbl%+41", [], "Bool"], ["declare-fun", "inline$UpdateValueMax$0$dstPath@0", [], "T@Path"], ["declare-fun", "inline$UpdateValue0$0$dstValue@0", [], "T@Value"], ["declare-fun", "%lbl%+42", [], "Bool"], ["declare-fun", "%lbl%+43", [], "Bool"], ["declare-fun", "%lbl%+44", [], "Bool"], ["declare-fun", "%lbl%+45", [], "Bool"], ["declare-fun", "inline$IsPrefixMax$0$isPrefix@1", [], "Bool"], ["declare-fun", "%lbl%+46", [], "Bool"], ["declare-fun", "%lbl%+47", [], "Bool"], ["declare-fun", "inline$IsPrefix0$0$isPrefix@1", [], "Bool"], ["declare-fun", "%lbl%+48", [], "Bool"], ["declare-fun", "%lbl%+49", [], "Bool"], ["declare-fun", "inline$IsPrefixMax$0$dstPath@0", [], "T@Path"], ["declare-fun", "%lbl%+50", [], "Bool"], ["declare-fun", "%lbl%+51", [], "Bool"], ["declare-fun", "inline$IsPrefixMax$0$srcPath@0", [], "T@Path"], ["declare-fun", "%lbl%+52", [], "Bool"], ["declare-fun", "%lbl%+53", [], "Bool"], ["declare-fun", "%lbl%+54", [], "Bool"], ["declare-fun", "%lbl%+55", [], "Bool"], ["declare-fun", "%lbl%+56", [], "Bool"], ["declare-fun", "%lbl%+57", [], "Bool"], ["declare-fun", "%lbl%+58", [], "Bool"], ["declare-fun", "%lbl%+59", [], "Bool"], ["declare-fun", "%lbl%+60", [], "Bool"], ["declare-fun", "|inline$WriteRef$0$to'@2|", [], "T@Reference"], ["declare-fun", "inline$LdConst$0$ret@1", [], "T@Value"], ["declare-fun", "%lbl%+61", [], "Bool"], ["declare-fun", "|inline$WriteRef$0$to'@1|", [], "T@Reference"], ["declare-fun", "%lbl%+62", [], "Bool"], ["declare-fun", "%lbl%+63", [], "Bool"], ["declare-fun", "|c'|", [], "Int"], ["declare-fun", "c", [], "Int"], ["declare-fun", "%lbl%+64", [], "Bool"], ["push", "1"], ["set-info", ":boogie-vc-id", "TestReference_mut_b"], ["assert", ["not", ["=>", ["=", ["ControlFlow", "0", "0"], "16187"], ["let", [["inline$UpdateValue0$1$anon3_Else_correct", ["=>", ["and", "%lbl%+0", "true"], "true"]]], ["let", [["inline$IsPrefix0$1$anon5_Else_correct", ["=>", ["and", "%lbl%+1", "true"], ["=>", ["not", ["=", "inline$IsPrefix0$1$srcPath@0", "Nil"]], ["or", "%lbl%@2", ["=>", ["=", ["ControlFlow", "0", "4205"], ["-", "0", "16915"]], "false"]]]]]], ["let", [["inline$UpdateValue0$0$anon3_Else_correct", ["=>", ["and", "%lbl%+3", "true"], "true"]]], ["let", [["inline$IsPrefix0$0$anon5_Else_correct", ["=>", ["and", "%lbl%+4", "true"], ["=>", ["not", ["=", "inline$IsPrefix0$0$srcPath@0", "Nil"]], ["or", "%lbl%@5", ["=>", ["=", ["ControlFlow", "0", "3647"], ["-", "0", "16619"]], "false"]]]]]], ["let", [["inline$DeepUpdateGlobal$0$anon2_Then$1_correct", ["=>", ["and", "%lbl%+6", "true"], "true"]]], ["let", [["inline$UpdateValueMax$2$anon3_Else$1_correct", ["=>", ["and", "%lbl%+7", "true"], ["=>", ["and", ["=", "|inline$UpdateValueMax$2$dstValue'@1|", ["Map", ["store", ["|m#Map|", "inline$UpdateValueMax$2$dstValue@0"], "inline$UpdateValueMax$2$e@0", "inline$UpdateValueMax$2$srcValue@0"]]], ["=", ["ControlFlow", "0", "4883"], "4919"]], "inline$DeepUpdateGlobal$0$anon2_Then$1_correct"]]]], ["let", [["inline$UpdateValue0$2$anon3_Then_correct", ["=>", ["and", "%lbl%+8", "true"], ["=>", ["and", ["=", "inline$UpdateValueMax$2$srcPath@0", "inline$UpdateValue0$2$dstPath@0"], ["=", ["ControlFlow", "0", "4863"], "4883"]], "inline$UpdateValueMax$2$anon3_Else$1_correct"]]]], ["let", [["inline$UpdateValueMax$2$anon3_Then_correct", ["=>", ["and", "%lbl%+9", "true"], ["=>", ["and", ["=", "inline$UpdateValueMax$2$srcPath@0", "inline$UpdateValueMax$2$dstPath@0"], ["=", ["ControlFlow", "0", "4893"], "4919"]], "inline$DeepUpdateGlobal$0$anon2_Then$1_correct"]]]], ["let", [["inline$UpdateValue0$2$anon3_Else_correct", ["=>", ["and", "%lbl%+10", "true"], "true"]]], ["let", [["inline$UpdateValue0$2$Entry_correct", ["=>", ["and", "%lbl%+11", "true"], ["=>", ["and", ["=", "inline$UpdateValue0$2$dstPath@0", ["Cons", "inline$UpdateValueMax$2$dstPath@0", "inline$UpdateValueMax$2$e@0"]], ["=", "inline$UpdateValue0$2$dstValue@0", ["select", ["|m#Map|", "inline$UpdateValueMax$2$dstValue@0"], "inline$UpdateValueMax$2$e@0"]]], ["and", ["=>", ["=", ["ControlFlow", "0", "4841"], "4863"], "inline$UpdateValue0$2$anon3_Then_correct"], ["=>", ["=", ["ControlFlow", "0", "4841"], "4853"], "inline$UpdateValue0$2$anon3_Else_correct"]]]]]], ["let", [["inline$UpdateValueMax$2$anon3_Else_correct", ["=>", ["and", "%lbl%+12", "true"], ["=>", ["and", ["not", ["=", "inline$UpdateValueMax$2$srcPath@0", "inline$UpdateValueMax$2$dstPath@0"]], ["=", ["ControlFlow", "0", "4869"], "4841"]], "inline$UpdateValue0$2$Entry_correct"]]]], ["let", [["inline$UpdateValueMax$2$Entry_correct", ["=>", ["and", "%lbl%+13", "true"], ["=>", ["and", ["and", ["=", "inline$UpdateValueMax$2$srcPath@0", ["|p#GlobalReference|", "|inline$WriteRef$0$to'@3|"]], ["=", "inline$UpdateValueMax$2$srcValue@0", ["|v#GlobalReference|", "|inline$WriteRef$0$to'@3|"]]], ["and", ["=", "inline$UpdateValueMax$2$dstPath@0", "Nil"], ["=", "inline$UpdateValueMax$2$dstValue@0", ["select", ["|contents#ResourceStore|", "rs_TestReference_T"], ["|a#GlobalReference|", "|inline$WriteRef$0$to'@3|"]]]]], ["and", ["=>", ["=", ["ControlFlow", "0", "4762"], "4893"], "inline$UpdateValueMax$2$anon3_Then_correct"], ["=>", ["=", ["ControlFlow", "0", "4762"], "4869"], "inline$UpdateValueMax$2$anon3_Else_correct"]]]]]], ["let", [["inline$DeepUpdateGlobal$0$anon2_Then_correct", ["=>", ["and", "%lbl%+14", "true"], ["=>", ["and", ["and", ["is-GlobalReference", "|inline$WriteRef$0$to'@3|"], ["=", "TestReference_T", ["|t#GlobalReference|", "|inline$WriteRef$0$to'@3|"]]], ["=", ["ControlFlow", "0", "4899"], "4762"]], "inline$UpdateValueMax$2$Entry_correct"]]]], ["let", [["inline$DeepUpdateGlobal$0$anon2_Else_correct", ["=>", ["and", "%lbl%+15", "true"], "true"]]], ["let", [["inline$DeepUpdateReference$0$anon9_Then$1_correct", ["=>", ["and", "%lbl%+16", "true"], ["=>", ["=", "|inline$DeepUpdateReference$0$dst'@2|", ["LocalReference", ["|c#LocalReference|", "arg0"], ["|l#LocalReference|", "arg0"], ["|p#LocalReference|", "arg0"], "|inline$UpdateValueMax$1$dstValue'|"]], ["and", ["=>", ["=", ["ControlFlow", "0", "4519"], "4899"], "inline$DeepUpdateGlobal$0$anon2_Then_correct"], ["=>", ["=", ["ControlFlow", "0", "4519"], "4649"], "inline$DeepUpdateGlobal$0$anon2_Else_correct"]]]]]], ["let", [["inline$UpdateValueMax$1$anon3_Else$1_correct", ["=>", ["and", "%lbl%+17", "true"], ["=>", ["and", ["=", "|inline$UpdateValueMax$1$dstValue'@1|", ["Map", ["store", ["|m#Map|", "inline$UpdateValueMax$1$dstValue@0"], "inline$UpdateValueMax$1$e@0", "inline$UpdateValueMax$1$srcValue@0"]]], ["=", ["ControlFlow", "0", "4485"], "4519"]], "inline$DeepUpdateReference$0$anon9_Then$1_correct"]]]], ["let", [["inline$UpdateValue0$1$anon3_Then_correct", ["=>", ["and", "%lbl%+18", "true"], ["=>", ["and", ["=", "inline$UpdateValueMax$1$srcPath@0", "inline$UpdateValue0$1$dstPath@0"], ["=", ["ControlFlow", "0", "4465"], "4485"]], "inline$UpdateValueMax$1$anon3_Else$1_correct"]]]], ["let", [["inline$UpdateValue0$1$Entry_correct", ["=>", ["and", "%lbl%+19", "true"], ["=>", ["and", ["=", "inline$UpdateValue0$1$dstPath@0", ["Cons", "inline$UpdateValueMax$1$dstPath@0", "inline$UpdateValueMax$1$e@0"]], ["=", "inline$UpdateValue0$1$dstValue@0", ["select", ["|m#Map|", "inline$UpdateValueMax$1$dstValue@0"], "inline$UpdateValueMax$1$e@0"]]], ["and", ["=>", ["=", ["ControlFlow", "0", "4443"], "4465"], "inline$UpdateValue0$1$anon3_Then_correct"], ["=>", ["=", ["ControlFlow", "0", "4443"], "4455"], "inline$UpdateValue0$1$anon3_Else_correct"]]]]]], ["let", [["inline$UpdateValueMax$1$anon3_Else_correct", ["=>", ["and", "%lbl%+20", "true"], ["=>", ["and", ["not", ["=", "inline$UpdateValueMax$1$srcPath@0", "inline$UpdateValueMax$1$dstPath@0"]], ["=", ["ControlFlow", "0", "4471"], "4443"]], "inline$UpdateValue0$1$Entry_correct"]]]], ["let", [["inline$UpdateValueMax$1$anon3_Then_correct", ["=>", ["and", "%lbl%+21", "true"], ["=>", ["and", ["=", "inline$UpdateValueMax$1$srcPath@0", "inline$UpdateValueMax$1$dstPath@0"], ["=", ["ControlFlow", "0", "4495"], "4519"]], "inline$DeepUpdateReference$0$anon9_Then$1_correct"]]]], ["let", [["inline$UpdateValueMax$1$Entry_correct", ["=>", ["and", "%lbl%+22", "true"], ["=>", ["and", ["and", ["=", "inline$UpdateValueMax$1$srcPath@0", ["|p#LocalReference|", "|inline$WriteRef$0$to'@3|"]], ["=", "inline$UpdateValueMax$1$srcValue@0", ["|v#LocalReference|", "|inline$WriteRef$0$to'@3|"]]], ["and", ["=", "inline$UpdateValueMax$1$dstPath@0", ["|p#LocalReference|", "arg0"]], ["=", "inline$UpdateValueMax$1$dstValue@0", ["|v#LocalReference|", "arg0"]]]], ["and", ["=>", ["=", ["ControlFlow", "0", "4364"], "4495"], "inline$UpdateValueMax$1$anon3_Then_correct"], ["=>", ["=", ["ControlFlow", "0", "4364"], "4471"], "inline$UpdateValueMax$1$anon3_Else_correct"]]]]]], ["let", [["inline$DeepUpdateReference$0$anon9_Then_correct", ["=>", ["and", "%lbl%+23", "true"], ["=>", ["and", "inline$IsPrefixMax$1$isPrefix@1", ["=", ["ControlFlow", "0", "4501"], "4364"]], "inline$UpdateValueMax$1$Entry_correct"]]]], ["let", [["inline$DeepUpdateReference$0$anon9_Else_correct", ["=>", ["and", "%lbl%+24", "true"], ["=>", ["not", "inline$IsPrefixMax$1$isPrefix@1"], ["and", ["=>", ["=", ["ControlFlow", "0", "4267"], "4899"], "inline$DeepUpdateGlobal$0$anon2_Then_correct"], ["=>", ["=", ["ControlFlow", "0", "4267"], "4649"], "inline$DeepUpdateGlobal$0$anon2_Else_correct"]]]]]], ["let", [["inline$IsPrefixMax$1$anon5_Else$1_correct", ["=>", ["and", "%lbl%+25", "true"], ["=>", ["and", ["=>", "inline$IsPrefixMax$1$isPrefix@1", "inline$IsPrefix0$1$isPrefix@1"], ["=>", "inline$IsPrefix0$1$isPrefix@1", "inline$IsPrefixMax$1$isPrefix@1"]], ["and", ["=>", ["=", ["ControlFlow", "0", "4233"], "4501"], "inline$DeepUpdateReference$0$anon9_Then_correct"], ["=>", ["=", ["ControlFlow", "0", "4233"], "4267"], "inline$DeepUpdateReference$0$anon9_Else_correct"]]]]]], ["let", [["inline$IsPrefix0$1$anon5_Then_correct", ["=>", ["and", "%lbl%+26", "true"], ["=>", ["=", "inline$IsPrefix0$1$srcPath@0", "Nil"], ["=>", ["and", ["and", ["=>", "inline$IsPrefix0$1$isPrefix@1", "false"], ["=>", "false", "inline$IsPrefix0$1$isPrefix@1"]], ["=", ["ControlFlow", "0", "4215"], "4233"]], "inline$IsPrefixMax$1$anon5_Else$1_correct"]]]]], ["let", [["inline$IsPrefix0$1$anon4_Else_correct", ["=>", ["and", "%lbl%+27", "true"], ["=>", ["not", ["=", "inline$IsPrefix0$1$srcPath@0", "inline$IsPrefixMax$1$dstPath@0"]], ["and", ["=>", ["=", ["ControlFlow", "0", "4195"], "4215"], "inline$IsPrefix0$1$anon5_Then_correct"], ["=>", ["=", ["ControlFlow", "0", "4195"], "4205"], "inline$IsPrefix0$1$anon5_Else_correct"]]]]]], ["let", [["inline$IsPrefix0$1$anon4_Then_correct", ["=>", ["and", "%lbl%+28", "true"], ["=>", ["=", "inline$IsPrefix0$1$srcPath@0", "inline$IsPrefixMax$1$dstPath@0"], ["=>", ["and", ["and", ["=>", "inline$IsPrefix0$1$isPrefix@1", "true"], ["=>", "true", "inline$IsPrefix0$1$isPrefix@1"]], ["=", ["ControlFlow", "0", "4225"], "4233"]], "inline$IsPrefixMax$1$anon5_Else$1_correct"]]]]], ["let", [["inline$IsPrefix0$1$Entry_correct", ["=>", ["and", "%lbl%+29", "true"], ["=>", ["=", "inline$IsPrefix0$1$srcPath@0", ["|p#Cons|", "inline$IsPrefixMax$1$srcPath@0"]], ["and", ["=>", ["=", ["ControlFlow", "0", "4185"], "4225"], "inline$IsPrefix0$1$anon4_Then_correct"], ["=>", ["=", ["ControlFlow", "0", "4185"], "4195"], "inline$IsPrefix0$1$anon4_Else_correct"]]]]]], ["let", [["inline$IsPrefixMax$1$anon5_Else_correct", ["=>", ["and", "%lbl%+30", "true"], ["=>", ["and", ["not", ["=", "inline$IsPrefixMax$1$srcPath@0", "Nil"]], ["=", ["ControlFlow", "0", "4231"], "4185"]], "inline$IsPrefix0$1$Entry_correct"]]]], ["let", [["inline$IsPrefixMax$1$anon5_Then_correct", ["=>", ["and", "%lbl%+31", "true"], ["=>", ["=", "inline$IsPrefixMax$1$srcPath@0", "Nil"], ["=>", ["and", ["=>", "inline$IsPrefixMax$1$isPrefix@1", "false"], ["=>", "false", "inline$IsPrefixMax$1$isPrefix@1"]], ["and", ["=>", ["=", ["ControlFlow", "0", "4243"], "4501"], "inline$DeepUpdateReference$0$anon9_Then_correct"], ["=>", ["=", ["ControlFlow", "0", "4243"], "4267"], "inline$DeepUpdateReference$0$anon9_Else_correct"]]]]]]], ["let", [["inline$IsPrefixMax$1$anon4_Else_correct", ["=>", ["and", "%lbl%+32", "true"], ["=>", ["not", ["=", "inline$IsPrefixMax$1$srcPath@0", "inline$IsPrefixMax$1$dstPath@0"]], ["and", ["=>", ["=", ["ControlFlow", "0", "4110"], "4243"], "inline$IsPrefixMax$1$anon5_Then_correct"], ["=>", ["=", ["ControlFlow", "0", "4110"], "4231"], "inline$IsPrefixMax$1$anon5_Else_correct"]]]]]], ["let", [["inline$IsPrefixMax$1$anon4_Then_correct", ["=>", ["and", "%lbl%+33", "true"], ["=>", ["=", "inline$IsPrefixMax$1$srcPath@0", "inline$IsPrefixMax$1$dstPath@0"], ["=>", ["and", ["=>", "inline$IsPrefixMax$1$isPrefix@1", "true"], ["=>", "true", "inline$IsPrefixMax$1$isPrefix@1"]], ["and", ["=>", ["=", ["ControlFlow", "0", "4253"], "4501"], "inline$DeepUpdateReference$0$anon9_Then_correct"], ["=>", ["=", ["ControlFlow", "0", "4253"], "4267"], "inline$DeepUpdateReference$0$anon9_Else_correct"]]]]]]], ["let", [["inline$IsPrefixMax$1$Entry_correct", ["=>", ["and", "%lbl%+34", "true"], ["=>", ["and", ["=", "inline$IsPrefixMax$1$dstPath@0", ["|p#LocalReference|", "arg0"]], ["=", "inline$IsPrefixMax$1$srcPath@0", ["|p#LocalReference|", "|inline$WriteRef$0$to'@3|"]]], ["and", ["=>", ["=", ["ControlFlow", "0", "4100"], "4253"], "inline$IsPrefixMax$1$anon4_Then_correct"], ["=>", ["=", ["ControlFlow", "0", "4100"], "4110"], "inline$IsPrefixMax$1$anon4_Else_correct"]]]]]], ["let", [["inline$DeepUpdateReference$0$anon8_Then_correct", ["=>", ["and", "%lbl%+35", "true"], ["=>", ["and", ["and", ["and", ["is-LocalReference", "arg0"], ["=", ["|c#LocalReference|", "|inline$WriteRef$0$to'@3|"], ["|c#LocalReference|", "arg0"]]], ["=", ["|l#LocalReference|", "|inline$WriteRef$0$to'@3|"], ["|l#LocalReference|", "arg0"]]], ["=", ["ControlFlow", "0", "4259"], "4100"]], "inline$IsPrefixMax$1$Entry_correct"]]]], ["let", [["inline$DeepUpdateReference$0$anon8_Else_correct", ["=>", ["and", "%lbl%+36", "true"], ["=>", ["not", ["and", ["and", ["is-LocalReference", "arg0"], ["=", ["|c#LocalReference|", "|inline$WriteRef$0$to'@3|"], ["|c#LocalReference|", "arg0"]]], ["=", ["|l#LocalReference|", "|inline$WriteRef$0$to'@3|"], ["|l#LocalReference|", "arg0"]]]], ["and", ["=>", ["=", ["ControlFlow", "0", "3999"], "4899"], "inline$DeepUpdateGlobal$0$anon2_Then_correct"], ["=>", ["=", ["ControlFlow", "0", "3999"], "4649"], "inline$DeepUpdateGlobal$0$anon2_Else_correct"]]]]]], ["let", [["inline$DeepUpdateReference$0$anon7_Then_correct", ["=>", ["and", "%lbl%+37", "true"], ["=>", ["is-LocalReference", "|inline$WriteRef$0$to'@3|"], ["and", ["=>", ["=", ["ControlFlow", "0", "3967"], "4259"], "inline$DeepUpdateReference$0$anon8_Then_correct"], ["=>", ["=", ["ControlFlow", "0", "3967"], "3999"], "inline$DeepUpdateReference$0$anon8_Else_correct"]]]]]], ["let", [["inline$DeepUpdateReference$0$anon11_Then$1_correct", ["=>", ["and", "%lbl%+38", "true"], ["=>", ["=", "|inline$DeepUpdateReference$0$dst'@1|", ["GlobalReference", ["|a#GlobalReference|", "arg0"], ["|t#GlobalReference|", "arg0"], ["|p#GlobalReference|", "arg0"], "|inline$UpdateValueMax$0$dstValue'|"]], ["and", ["=>", ["=", ["ControlFlow", "0", "3961"], "4899"], "inline$DeepUpdateGlobal$0$anon2_Then_correct"], ["=>", ["=", ["ControlFlow", "0", "3961"], "4649"], "inline$DeepUpdateGlobal$0$anon2_Else_correct"]]]]]], ["let", [["inline$UpdateValueMax$0$anon3_Else$1_correct", ["=>", ["and", "%lbl%+39", "true"], ["=>", ["and", ["=", "|inline$UpdateValueMax$0$dstValue'@1|", ["Map", ["store", ["|m#Map|", "inline$UpdateValueMax$0$dstValue@0"], "inline$UpdateValueMax$0$e@0", "inline$UpdateValueMax$0$srcValue@0"]]], ["=", ["ControlFlow", "0", "3927"], "3961"]], "inline$DeepUpdateReference$0$anon11_Then$1_correct"]]]], ["let", [["inline$UpdateValue0$0$anon3_Then_correct", ["=>", ["and", "%lbl%+40", "true"], ["=>", ["and", ["=", "inline$UpdateValueMax$0$srcPath@0", "inline$UpdateValue0$0$dstPath@0"], ["=", ["ControlFlow", "0", "3907"], "3927"]], "inline$UpdateValueMax$0$anon3_Else$1_correct"]]]], ["let", [["inline$UpdateValue0$0$Entry_correct", ["=>", ["and", "%lbl%+41", "true"], ["=>", ["and", ["=", "inline$UpdateValue0$0$dstPath@0", ["Cons", "inline$UpdateValueMax$0$dstPath@0", "inline$UpdateValueMax$0$e@0"]], ["=", "inline$UpdateValue0$0$dstValue@0", ["select", ["|m#Map|", "inline$UpdateValueMax$0$dstValue@0"], "inline$UpdateValueMax$0$e@0"]]], ["and", ["=>", ["=", ["ControlFlow", "0", "3885"], "3907"], "inline$UpdateValue0$0$anon3_Then_correct"], ["=>", ["=", ["ControlFlow", "0", "3885"], "3897"], "inline$UpdateValue0$0$anon3_Else_correct"]]]]]], ["let", [["inline$UpdateValueMax$0$anon3_Else_correct", ["=>", ["and", "%lbl%+42", "true"], ["=>", ["and", ["not", ["=", "inline$UpdateValueMax$0$srcPath@0", "inline$UpdateValueMax$0$dstPath@0"]], ["=", ["ControlFlow", "0", "3913"], "3885"]], "inline$UpdateValue0$0$Entry_correct"]]]], ["let", [["inline$UpdateValueMax$0$anon3_Then_correct", ["=>", ["and", "%lbl%+43", "true"], ["=>", ["and", ["=", "inline$UpdateValueMax$0$srcPath@0", "inline$UpdateValueMax$0$dstPath@0"], ["=", ["ControlFlow", "0", "3937"], "3961"]], "inline$DeepUpdateReference$0$anon11_Then$1_correct"]]]], ["let", [["inline$UpdateValueMax$0$Entry_correct", ["=>", ["and", "%lbl%+44", "true"], ["=>", ["and", ["and", ["=", "inline$UpdateValueMax$0$srcPath@0", ["|p#GlobalReference|", "|inline$WriteRef$0$to'@3|"]], ["=", "inline$UpdateValueMax$0$srcValue@0", ["|v#GlobalReference|", "|inline$WriteRef$0$to'@3|"]]], ["and", ["=", "inline$UpdateValueMax$0$dstPath@0", ["|p#GlobalReference|", "arg0"]], ["=", "inline$UpdateValueMax$0$dstValue@0", ["|v#GlobalReference|", "arg0"]]]], ["and", ["=>", ["=", ["ControlFlow", "0", "3806"], "3937"], "inline$UpdateValueMax$0$anon3_Then_correct"], ["=>", ["=", ["ControlFlow", "0", "3806"], "3913"], "inline$UpdateValueMax$0$anon3_Else_correct"]]]]]], ["let", [["inline$DeepUpdateReference$0$anon11_Then_correct", ["=>", ["and", "%lbl%+45", "true"], ["=>", ["and", "inline$IsPrefixMax$0$isPrefix@1", ["=", ["ControlFlow", "0", "3943"], "3806"]], "inline$UpdateValueMax$0$Entry_correct"]]]], ["let", [["inline$DeepUpdateReference$0$anon11_Else_correct", ["=>", ["and", "%lbl%+46", "true"], ["=>", ["not", "inline$IsPrefixMax$0$isPrefix@1"], ["and", ["=>", ["=", ["ControlFlow", "0", "3709"], "4899"], "inline$DeepUpdateGlobal$0$anon2_Then_correct"], ["=>", ["=", ["ControlFlow", "0", "3709"], "4649"], "inline$DeepUpdateGlobal$0$anon2_Else_correct"]]]]]], ["let", [["inline$IsPrefixMax$0$anon5_Else$1_correct", ["=>", ["and", "%lbl%+47", "true"], ["=>", ["and", ["=>", "inline$IsPrefixMax$0$isPrefix@1", "inline$IsPrefix0$0$isPrefix@1"], ["=>", "inline$IsPrefix0$0$isPrefix@1", "inline$IsPrefixMax$0$isPrefix@1"]], ["and", ["=>", ["=", ["ControlFlow", "0", "3675"], "3943"], "inline$DeepUpdateReference$0$anon11_Then_correct"], ["=>", ["=", ["ControlFlow", "0", "3675"], "3709"], "inline$DeepUpdateReference$0$anon11_Else_correct"]]]]]], ["let", [["inline$IsPrefix0$0$anon5_Then_correct", ["=>", ["and", "%lbl%+48", "true"], ["=>", ["=", "inline$IsPrefix0$0$srcPath@0", "Nil"], ["=>", ["and", ["and", ["=>", "inline$IsPrefix0$0$isPrefix@1", "false"], ["=>", "false", "inline$IsPrefix0$0$isPrefix@1"]], ["=", ["ControlFlow", "0", "3657"], "3675"]], "inline$IsPrefixMax$0$anon5_Else$1_correct"]]]]], ["let", [["inline$IsPrefix0$0$anon4_Else_correct", ["=>", ["and", "%lbl%+49", "true"], ["=>", ["not", ["=", "inline$IsPrefix0$0$srcPath@0", "inline$IsPrefixMax$0$dstPath@0"]], ["and", ["=>", ["=", ["ControlFlow", "0", "3637"], "3657"], "inline$IsPrefix0$0$anon5_Then_correct"], ["=>", ["=", ["ControlFlow", "0", "3637"], "3647"], "inline$IsPrefix0$0$anon5_Else_correct"]]]]]], ["let", [["inline$IsPrefix0$0$anon4_Then_correct", ["=>", ["and", "%lbl%+50", "true"], ["=>", ["=", "inline$IsPrefix0$0$srcPath@0", "inline$IsPrefixMax$0$dstPath@0"], ["=>", ["and", ["and", ["=>", "inline$IsPrefix0$0$isPrefix@1", "true"], ["=>", "true", "inline$IsPrefix0$0$isPrefix@1"]], ["=", ["ControlFlow", "0", "3667"], "3675"]], "inline$IsPrefixMax$0$anon5_Else$1_correct"]]]]], ["let", [["inline$IsPrefix0$0$Entry_correct", ["=>", ["and", "%lbl%+51", "true"], ["=>", ["=", "inline$IsPrefix0$0$srcPath@0", ["|p#Cons|", "inline$IsPrefixMax$0$srcPath@0"]], ["and", ["=>", ["=", ["ControlFlow", "0", "3627"], "3667"], "inline$IsPrefix0$0$anon4_Then_correct"], ["=>", ["=", ["ControlFlow", "0", "3627"], "3637"], "inline$IsPrefix0$0$anon4_Else_correct"]]]]]], ["let", [["inline$IsPrefixMax$0$anon5_Else_correct", ["=>", ["and", "%lbl%+52", "true"], ["=>", ["and", ["not", ["=", "inline$IsPrefixMax$0$srcPath@0", "Nil"]], ["=", ["ControlFlow", "0", "3673"], "3627"]], "inline$IsPrefix0$0$Entry_correct"]]]], ["let", [["inline$IsPrefixMax$0$anon5_Then_correct", ["=>", ["and", "%lbl%+53", "true"], ["=>", ["=", "inline$IsPrefixMax$0$srcPath@0", "Nil"], ["=>", ["and", ["=>", "inline$IsPrefixMax$0$isPrefix@1", "false"], ["=>", "false", "inline$IsPrefixMax$0$isPrefix@1"]], ["and", ["=>", ["=", ["ControlFlow", "0", "3685"], "3943"], "inline$DeepUpdateReference$0$anon11_Then_correct"], ["=>", ["=", ["ControlFlow", "0", "3685"], "3709"], "inline$DeepUpdateReference$0$anon11_Else_correct"]]]]]]], ["let", [["inline$IsPrefixMax$0$anon4_Else_correct", ["=>", ["and", "%lbl%+54", "true"], ["=>", ["not", ["=", "inline$IsPrefixMax$0$srcPath@0", "inline$IsPrefixMax$0$dstPath@0"]], ["and", ["=>", ["=", ["ControlFlow", "0", "3552"], "3685"], "inline$IsPrefixMax$0$anon5_Then_correct"], ["=>", ["=", ["ControlFlow", "0", "3552"], "3673"], "inline$IsPrefixMax$0$anon5_Else_correct"]]]]]], ["let", [["inline$IsPrefixMax$0$anon4_Then_correct", ["=>", ["and", "%lbl%+55", "true"], ["=>", ["=", "inline$IsPrefixMax$0$srcPath@0", "inline$IsPrefixMax$0$dstPath@0"], ["=>", ["and", ["=>", "inline$IsPrefixMax$0$isPrefix@1", "true"], ["=>", "true", "inline$IsPrefixMax$0$isPrefix@1"]], ["and", ["=>", ["=", ["ControlFlow", "0", "3695"], "3943"], "inline$DeepUpdateReference$0$anon11_Then_correct"], ["=>", ["=", ["ControlFlow", "0", "3695"], "3709"], "inline$DeepUpdateReference$0$anon11_Else_correct"]]]]]]], ["let", [["inline$IsPrefixMax$0$Entry_correct", ["=>", ["and", "%lbl%+56", "true"], ["=>", ["and", ["=", "inline$IsPrefixMax$0$dstPath@0", ["|p#GlobalReference|", "arg0"]], ["=", "inline$IsPrefixMax$0$srcPath@0", ["|p#GlobalReference|", "|inline$WriteRef$0$to'@3|"]]], ["and", ["=>", ["=", ["ControlFlow", "0", "3542"], "3695"], "inline$IsPrefixMax$0$anon4_Then_correct"], ["=>", ["=", ["ControlFlow", "0", "3542"], "3552"], "inline$IsPrefixMax$0$anon4_Else_correct"]]]]]], ["let", [["inline$DeepUpdateReference$0$anon10_Then_correct", ["=>", ["and", "%lbl%+57", "true"], ["=>", ["and", ["and", ["and", ["is-GlobalReference", "arg0"], ["=", ["|a#GlobalReference|", "|inline$WriteRef$0$to'@3|"], ["|a#GlobalReference|", "arg0"]]], ["=", ["|t#GlobalReference|", "|inline$WriteRef$0$to'@3|"], ["|t#GlobalReference|", "arg0"]]], ["=", ["ControlFlow", "0", "3701"], "3542"]], "inline$IsPrefixMax$0$Entry_correct"]]]], ["let", [["inline$DeepUpdateReference$0$anon10_Else_correct", ["=>", ["and", "%lbl%+58", "true"], ["=>", ["not", ["and", ["and", ["is-GlobalReference", "arg0"], ["=", ["|a#GlobalReference|", "|inline$WriteRef$0$to'@3|"], ["|a#GlobalReference|", "arg0"]]], ["=", ["|t#GlobalReference|", "|inline$WriteRef$0$to'@3|"], ["|t#GlobalReference|", "arg0"]]]], ["and", ["=>", ["=", ["ControlFlow", "0", "3441"], "4899"], "inline$DeepUpdateGlobal$0$anon2_Then_correct"], ["=>", ["=", ["ControlFlow", "0", "3441"], "4649"], "inline$DeepUpdateGlobal$0$anon2_Else_correct"]]]]]], ["let", [["inline$DeepUpdateReference$0$anon7_Else_correct", ["=>", ["and", "%lbl%+59", "true"], ["=>", ["not", ["is-LocalReference", "|inline$WriteRef$0$to'@3|"]], ["and", ["=>", ["=", ["ControlFlow", "0", "3409"], "3701"], "inline$DeepUpdateReference$0$anon10_Then_correct"], ["=>", ["=", ["ControlFlow", "0", "3409"], "3441"], "inline$DeepUpdateReference$0$anon10_Else_correct"]]]]]], ["let", [["inline$WriteRef$0$anon3_Else_correct", ["=>", ["and", "%lbl%+60", "true"], ["=>", ["not", ["is-GlobalReference", "arg0"]], ["=>", ["and", ["=", "|inline$WriteRef$0$to'@2|", ["LocalReference", ["|c#LocalReference|", "arg0"], ["|l#LocalReference|", "arg0"], ["|p#LocalReference|", "arg0"], "inline$LdConst$0$ret@1"]], ["=", "|inline$WriteRef$0$to'@3|", "|inline$WriteRef$0$to'@2|"]], ["and", ["=>", ["=", ["ControlFlow", "0", "3125"], "3967"], "inline$DeepUpdateReference$0$anon7_Then_correct"], ["=>", ["=", ["ControlFlow", "0", "3125"], "3409"], "inline$DeepUpdateReference$0$anon7_Else_correct"]]]]]]], ["let", [["inline$WriteRef$0$anon3_Then_correct", ["=>", ["and", "%lbl%+61", "true"], ["=>", ["is-GlobalReference", "arg0"], ["=>", ["and", ["=", "|inline$WriteRef$0$to'@1|", ["GlobalReference", ["|a#GlobalReference|", "arg0"], ["|t#GlobalReference|", "arg0"], ["|p#GlobalReference|", "arg0"], "inline$LdConst$0$ret@1"]], ["=", "|inline$WriteRef$0$to'@3|", "|inline$WriteRef$0$to'@1|"]], ["and", ["=>", ["=", ["ControlFlow", "0", "3147"], "3967"], "inline$DeepUpdateReference$0$anon7_Then_correct"], ["=>", ["=", ["ControlFlow", "0", "3147"], "3409"], "inline$DeepUpdateReference$0$anon7_Else_correct"]]]]]]], ["let", [["inline$LdConst$0$anon0_correct", ["=>", ["and", "%lbl%+62", "true"], ["=>", ["=", "inline$LdConst$0$ret@1", ["Integer", "0"]], ["and", ["=>", ["=", ["ControlFlow", "0", "2992"], "3147"], "inline$WriteRef$0$anon3_Then_correct"], ["=>", ["=", ["ControlFlow", "0", "2992"], "3125"], "inline$WriteRef$0$anon3_Else_correct"]]]]]], ["let", [["anon0_correct", ["=>", ["and", "%lbl%+63", "true"], ["=>", ["and", [">", "|c'|", "c"], ["=", ["ControlFlow", "0", "2998"], "2992"]], "inline$LdConst$0$anon0_correct"]]]], ["let", [["PreconditionGeneratedEntry_correct", ["=>", ["and", "%lbl%+64", "true"], ["=>", ["=", ["ControlFlow", "0", "16187"], "2998"], "anon0_correct"]]]], "PreconditionGeneratedEntry_correct"]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]], ["check-sat"]]
  7. ''')
  8.  
  9. def generate_mutations(original):
  10.     for node in original:
  11.         yield original
  12.  
  13. def check(task):
  14.     return task
  15.  
  16. if __name__ == "__main__":
  17.     logger = log_to_stderr()
  18.     logger.setLevel(logging.DEBUG)
  19.  
  20.     while True:
  21.         with Pool(2) as pool:
  22.             for result in pool.imap(check, generate_mutations(DATA)):
  23.             #for result in map(check, generate_mutations(DATA)):
  24.                 print("Stopping")
  25.                 break
  26.             print("Loop is done")
  27.         print("Processing is done")
  28.  
Advertisement
Add Comment
Please, Sign In to add comment
Public Pastes
We use cookies for various purposes including analytics. By continuing to use Pastebin, you agree to our use of cookies as described in the Cookies Policy.  OK, I Understand
Not a member of Pastebin yet?
Sign Up, it unlocks many cool features!