Last active
October 14, 2024 14:53
-
-
Save wolfspider/7ecec764d8cf5988d46f246bb0468f7f to your computer and use it in GitHub Desktop.
Bosque Scheduler
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| namespace NSMain; | |
| entity Func { | |
| invariant $lf != ""; | |
| field lf: String; | |
| factory static enqueue(f: fn() -> String): | |
| { lf: String } | |
| { | |
| return { lf = f() }; | |
| } | |
| override method exe(): String | |
| { | |
| return this.lf; | |
| } | |
| } | |
| function checkIntBounds(arg: Int?): Bool { | |
| //reduce the number of values for scheduling | |
| return arg == none || ((arg >= 0) && (arg <= 10)); | |
| } | |
| concept Scheduler { | |
| abstract method schedule(func: Func): Scheduler; | |
| abstract method delay(timeout: Int, func: Func): Scheduler; | |
| } | |
| entity TestScheduler provides Scheduler { | |
| field now: Int; | |
| field currentTime: Int; | |
| field timeline: Map<Int, List<Func>>; | |
| field running: Bool; | |
| field runlist: List<{time: Int, func: Func}>; | |
| field sortedTasks: List<{time: Int, func: Func}>; | |
| // Constructor | |
| factory static new(): | |
| { | |
| now: Int, | |
| currentTime: Int, | |
| timeline: Map<Int, List<Func>>, | |
| running: Bool, | |
| runlist: List<{time: Int, func: Func}>, | |
| sortedTasks: List<{time: Int, func: Func}> | |
| } | |
| { | |
| return { | |
| now = 0, | |
| currentTime = 0, | |
| timeline = Map<Int, List<Func>>@{}, | |
| running = false, | |
| runlist = List<{time: Int, func: Func}>@{}, | |
| sortedTasks = List<{time: Int, func: Func}>@{} | |
| }; | |
| } | |
| // Schedule function to add to the timeline | |
| method usched(delay: Int, func: Func): TestScheduler { | |
| let at = this.currentTime + delay; | |
| let updatedTimeline = (this.timeline.has(at)) ? Map<Int, List<Func>>@{ | |
| this.timeline.keys().get(at) => | |
| this.timeline.get(at).append(List<Func>@{func}) | |
| } : Map<Int, List<Func>>@{ | |
| at => List<Func>@{func} | |
| }; | |
| // Filter tasks that should come before and after the new task | |
| let tasksBefore = this.sortedTasks.filter(fn(task) => task.time < at); | |
| let tasksAfter = this.sortedTasks.filter(fn(task) => task.time >= at); | |
| return this.update | |
| ( | |
| timeline = updatedTimeline, | |
| sortedTasks = tasksBefore | |
| .append(List<{time: Int, func: Func}>@{{time=at,func=func}}) | |
| .append(tasksAfter) | |
| ); | |
| } | |
| // Run function to process scheduled functions | |
| method run(): TestScheduler { | |
| if (this.timeline.empty()) { | |
| //_debug("I'm empty"); | |
| return this.update | |
| ( | |
| running = false | |
| ); | |
| } | |
| let r = this.update | |
| ( | |
| currentTime = this.now, | |
| runlist = this.sortedTasks, | |
| sortedTasks = List<{time: Int, func: Func}>@{} | |
| ); | |
| return r; | |
| } | |
| // Returns the current time | |
| method utcnow(): Int { | |
| return this.currentTime; | |
| } | |
| // Schedule immediately | |
| method schedule(func: Func): TestScheduler { | |
| let sch = this.usched(this.currentTime, func); | |
| if (!this.running) { | |
| let r = this.update | |
| ( | |
| running = true, | |
| sortedTasks = sch.sortedTasks | |
| ); | |
| return r; | |
| } | |
| return sch; | |
| } | |
| // Delay schedule | |
| method delay(timeout: Int, func: Func): TestScheduler | |
| requires release checkIntBounds(timeout); | |
| { | |
| let sch = this.usched(timeout, func); | |
| return sch; | |
| } | |
| } | |
| entrypoint function main(): Any { | |
| // Schedule task1 to run immediately | |
| let s = TestScheduler@new() | |
| .schedule(Func@enqueue(fn() => "R1")) | |
| .delay(18, Func@enqueue(fn() => "R2")) | |
| .delay(2, Func@enqueue(fn() => "R3")) | |
| .run(); | |
| let currentTime = s.utcnow(); | |
| check currentTime == s.now; | |
| check s.runlist.get(0).func.exe() == "R1"; | |
| check s.runlist.get(1).func.exe() == "R3"; | |
| check s.runlist.get(2).func.exe() == "R2"; | |
| return [s.runlist, currentTime]; | |
| } |
;;-------------------------------------------------------------------------------------------------------
;; Copyright (C) Microsoft. All rights reserved.
;; Licensed under the MIT license. See LICENSE.txt file in the project root for full license information.
;;-------------------------------------------------------------------------------------------------------
(set-option :smt.auto-config false) ; disable automatic self configuration
(set-option :smt.mbqi false) ; disable model-based quantifier instantiation
(set-option :timeout 10000)
(declare-datatypes (
(StructuralSpecialTypeInfo 0)
) (
( (StructuralSpecialTypeInfo@cons (StructuralSpecialTypeInfo$PODType Bool) (StructuralSpecialTypeInfo$APIType Bool) (StructuralSpecialTypeInfo$Parsable Bool)) )
))
(declare-datatypes (
(bsq_safestring 0)
(bsq_stringof 0)
(bsq_uuid 0)
(bsq_logicaltime 0)
(bsq_cryptohash 0)
(bsq_enum 0)
(bsq_idkeysimple 0)
(bsq_idkeycompound 0)
(BKeyValue 0)
) (
( (bsq_safestring@cons (bsq_safestring_type Int) (bsq_safestring_value String)) )
( (bsq_stringof@cons (bsq_stringof_type Int) (bsq_stringof_value String)) )
( (bsq_uuid@cons (bsq_uuid_value String)) )
( (bsq_logicaltime@cons (bsq_logicaltime_value Int)) )
( (bsq_cryptohash@cons (bsq_cryptohash_value String)) )
( (bsq_enum@cons (bsq_enum_type Int) (bsq_enum_value Int)) )
( (bsq_idkeysimple@cons (bsq_idkeysimple_type Int) (bsq_idkeysimple_value BKeyValue)) )
( (bsq_idkeycompound@cons (bsq_idkeycompound_type Int) (bsq_idkeycompound_value (Array Int BKeyValue))) )
(
(bsqkey_none)
(bsqkey_bool (bsqkey_bool_value Bool))
(bsqkey_int (bsqkey_int_value Int))
(bsqkey_bigint (bsqkey_bigint_value Int))
(bsqkey_string (bsqkey_string_value String))
(bsqkey_safestring (bsqkey_safestring_value bsq_safestring))
(bsqkey_stringof (bsqkey_stringof_value bsq_stringof))
(bsqkey_uuid (bsqkey_uuid_value bsq_uuid))
(bsqkey_logicaltime (bsqkey_logicaltime_value bsq_logicaltime))
(bsqkey_cryptohash (bsqkey_cryptohash_value bsq_cryptohash))
(bsqkey_enum (bsqkey_enum_value bsq_enum))
(bsqkey_idkeysimple (bsqkey_idkeysimple_value bsq_idkeysimple))
(bsqkey_idkeycompound (bsqkey_idkeycompound_value bsq_idkeycompound))
)
))
(declare-datatypes (
(bsq_buffer 0)
(bsq_bufferof 0)
(bsq_bytebuffer 0)
(bsq_isotime 0)
(bsq_regex 0)
(bsq_tuple 0)
(bsq_record 0)
(nscore__assumesafeI0I 0)
(nscore__keylist_k_nscore__int_I11I 0)
(nscore__knownsafeI14I 0)
(nscore__list_t__func_nsmain__func__time_nscore__int__I15I 0)
(nscore__list_t_nscore__int_I17I 0)
(nscore__list_t_nsmain__func_I19I 0)
(nscore__map_k_nscore__int__v_nscore__list_nsmain__func__I23I 0)
(nscore__mapentry_k_nscore__int__v_nscore__list_nsmain__func__I26I 0)
(nsmain__funcI20I 0)
(nsmain__testschedulerI34I 0)
(bsq_object 0)
(BTerm 0)
) (
( (bsq_buffer@cons (bsq_buffer_type Int) (bsq_buffer_contents String)) )
( (bsq_bufferof@cons (bsq_bufferof_type Int) (bsq_bufferof_contents String)) )
( (bsq_bytebuffer@cons (bsq_bytebuffer_contents (Seq Int))) )
( (bsq_isotime@cons (bsq_isotime_value Int)) )
( (bsq_regex@cons (bsq_regex_value Int)) )
( (bsq_tuple@cons (bsq_tuple_concepts StructuralSpecialTypeInfo) (bsq_tuple_entries (Array Int BTerm))) )
( (bsq_record@cons (bsq_record_concepts StructuralSpecialTypeInfo) (bsq_record_entries (Array String BTerm))) )
( (nscore__assumesafeI0I@cons ) )
( (nscore__keylist_k_nscore__int_I11I@cons (nscore__keylist_k_nscore__int_I11I@nscore__keylist_k_nscore__int__hkeyI12I Int) (nscore__keylist_k_nscore__int_I11I@nscore__keylist_k_nscore__int__tailI13I BTerm)) )
( (nscore__knownsafeI14I@cons ) )
( (nscore__list_t__func_nsmain__func__time_nscore__int__I15I@cons (nscore__list_t__func_nsmain__func__time_nscore__int__I15I@@size Int) (nscore__list_t__func_nsmain__func__time_nscore__int__I15I@@entries (Array Int bsq_record))) )
( (nscore__list_t_nscore__int_I17I@cons (nscore__list_t_nscore__int_I17I@@size Int) (nscore__list_t_nscore__int_I17I@@entries (Array Int Int))) )
( (nscore__list_t_nsmain__func_I19I@cons (nscore__list_t_nsmain__func_I19I@@size Int) (nscore__list_t_nsmain__func_I19I@@entries (Array Int nsmain__funcI20I))) )
( (nscore__map_k_nscore__int__v_nscore__list_nsmain__func__I23I@cons (nscore__map_k_nscore__int__v_nscore__list_nsmain__func__I23I@@size Int) (nscore__map_k_nscore__int__v_nscore__list_nsmain__func__I23I@@has (Array Int Bool)) (nscore__map_k_nscore__int__v_nscore__list_nsmain__func__I23I@@values (Array Int nscore__list_t_nsmain__func_I19I)) (nscore__map_k_nscore__int__v_nscore__list_nsmain__func__I23I@@keylist BTerm)) )
( (nscore__mapentry_k_nscore__int__v_nscore__list_nsmain__func__I26I@cons (nscore__mapentry_k_nscore__int__v_nscore__list_nsmain__func__I26I@nscore__mapentry_k_nscore__int__v_nscore__list_nsmain__func___keyI27I Int) (nscore__mapentry_k_nscore__int__v_nscore__list_nsmain__func__I26I@nscore__mapentry_k_nscore__int__v_nscore__list_nsmain__func___valueI28I nscore__list_t_nsmain__func_I19I)) )
( (nsmain__funcI20I@cons (nsmain__funcI20I@nsmain__func_lfI33I String)) )
( (nsmain__testschedulerI34I@cons (nsmain__testschedulerI34I@nsmain__testscheduler_nowI35I Int) (nsmain__testschedulerI34I@nsmain__testscheduler_currenttimeI36I Int) (nsmain__testschedulerI34I@nsmain__testscheduler_timelineI37I nscore__map_k_nscore__int__v_nscore__list_nsmain__func__I23I) (nsmain__testschedulerI34I@nsmain__testscheduler_runningI38I Bool) (nsmain__testschedulerI34I@nsmain__testscheduler_runlistI39I nscore__list_t__func_nsmain__func__time_nscore__int__I15I) (nsmain__testschedulerI34I@nsmain__testscheduler_sortedtasksI40I nscore__list_t__func_nsmain__func__time_nscore__int__I15I)) )
(
(bsq_object@empty)
(cons@bsq_object_from_nscore__assumesafeI0I (bsqterm_object_nscore__assumesafeI0I_value nscore__assumesafeI0I))
(cons@bsq_object_from_nscore__keylist_k_nscore__int_I11I (bsqterm_object_nscore__keylist_k_nscore__int_I11I_value nscore__keylist_k_nscore__int_I11I))
(cons@bsq_object_from_nscore__knownsafeI14I (bsqterm_object_nscore__knownsafeI14I_value nscore__knownsafeI14I))
(cons@bsq_object_from_nscore__list_t__func_nsmain__func__time_nscore__int__I15I (bsqterm_object_nscore__list_t__func_nsmain__func__time_nscore__int__I15I_value nscore__list_t__func_nsmain__func__time_nscore__int__I15I))
(cons@bsq_object_from_nscore__list_t_nscore__int_I17I (bsqterm_object_nscore__list_t_nscore__int_I17I_value nscore__list_t_nscore__int_I17I))
(cons@bsq_object_from_nscore__list_t_nsmain__func_I19I (bsqterm_object_nscore__list_t_nsmain__func_I19I_value nscore__list_t_nsmain__func_I19I))
(cons@bsq_object_from_nscore__map_k_nscore__int__v_nscore__list_nsmain__func__I23I (bsqterm_object_nscore__map_k_nscore__int__v_nscore__list_nsmain__func__I23I_value nscore__map_k_nscore__int__v_nscore__list_nsmain__func__I23I))
(cons@bsq_object_from_nscore__mapentry_k_nscore__int__v_nscore__list_nsmain__func__I26I (bsqterm_object_nscore__mapentry_k_nscore__int__v_nscore__list_nsmain__func__I26I_value nscore__mapentry_k_nscore__int__v_nscore__list_nsmain__func__I26I))
(cons@bsq_object_from_nsmain__funcI20I (bsqterm_object_nsmain__funcI20I_value nsmain__funcI20I))
(cons@bsq_object_from_nsmain__testschedulerI34I (bsqterm_object_nsmain__testschedulerI34I_value nsmain__testschedulerI34I))
)
(
(bsqterm@clear)
(bsqterm_key (bsqterm_key_value BKeyValue))
(bsqterm_float64 (bsqterm_float64_value (_ FloatingPoint 11 53)))
(bsqterm_buffer (bsqterm_buffer_value bsq_buffer))
(bsqterm_bufferof (bsqterm_bufferof_value bsq_bufferof))
(bsqterm_bytebuffer (bsqterm_bytebuffer_value bsq_bytebuffer))
(bsqterm_isotime (bsqterm_isotime_value bsq_isotime))
(bsqterm_regex (bsqterm_regex_value bsq_regex))
(bsqterm_tuple (bsqterm_tuple_value bsq_tuple))
(bsqterm_record (bsqterm_record_value bsq_record))
(bsqterm_object (bsqterm_object_type Int) (bsqterm_object_value bsq_object))
)
))
(declare-const MIRNominalTypeEnum_nscore__assumesafeI0I Int)
(assert (= MIRNominalTypeEnum_nscore__assumesafeI0I 1))
(declare-const MIRNominalTypeEnum_nscore__bigintI1I Int)
(assert (= MIRNominalTypeEnum_nscore__bigintI1I 3))
(declare-const MIRNominalTypeEnum_nscore__boolI2I Int)
(assert (= MIRNominalTypeEnum_nscore__boolI2I 5))
(declare-const MIRNominalTypeEnum_nscore__buffercompressionI3I Int)
(assert (= MIRNominalTypeEnum_nscore__buffercompressionI3I 7))
(declare-const MIRNominalTypeEnum_nscore__bufferencodingI4I Int)
(assert (= MIRNominalTypeEnum_nscore__bufferencodingI4I 9))
(declare-const MIRNominalTypeEnum_nscore__bufferformatI5I Int)
(assert (= MIRNominalTypeEnum_nscore__bufferformatI5I 11))
(declare-const MIRNominalTypeEnum_nscore__bytebufferI6I Int)
(assert (= MIRNominalTypeEnum_nscore__bytebufferI6I 13))
(declare-const MIRNominalTypeEnum_nscore__cryptohashI7I Int)
(assert (= MIRNominalTypeEnum_nscore__cryptohashI7I 15))
(declare-const MIRNominalTypeEnum_nscore__float64I8I Int)
(assert (= MIRNominalTypeEnum_nscore__float64I8I 17))
(declare-const MIRNominalTypeEnum_nscore__intI9I Int)
(assert (= MIRNominalTypeEnum_nscore__intI9I 19))
(declare-const MIRNominalTypeEnum_nscore__isotimeI10I Int)
(assert (= MIRNominalTypeEnum_nscore__isotimeI10I 21))
(declare-const MIRNominalTypeEnum_nscore__keylist_k_nscore__int_I11I Int)
(assert (= MIRNominalTypeEnum_nscore__keylist_k_nscore__int_I11I 23))
(declare-const MIRNominalTypeEnum_nscore__knownsafeI14I Int)
(assert (= MIRNominalTypeEnum_nscore__knownsafeI14I 25))
(declare-const MIRNominalTypeEnum_nscore__list_t__func_nsmain__func__time_nscore__int__I15I Int)
(assert (= MIRNominalTypeEnum_nscore__list_t__func_nsmain__func__time_nscore__int__I15I 27))
(declare-const MIRNominalTypeEnum_nscore__list_t_nscore__int_I17I Int)
(assert (= MIRNominalTypeEnum_nscore__list_t_nscore__int_I17I 29))
(declare-const MIRNominalTypeEnum_nscore__list_t_nsmain__func_I19I Int)
(assert (= MIRNominalTypeEnum_nscore__list_t_nsmain__func_I19I 31))
(declare-const MIRNominalTypeEnum_nscore__logicaltimeI22I Int)
(assert (= MIRNominalTypeEnum_nscore__logicaltimeI22I 33))
(declare-const MIRNominalTypeEnum_nscore__map_k_nscore__int__v_nscore__list_nsmain__func__I23I Int)
(assert (= MIRNominalTypeEnum_nscore__map_k_nscore__int__v_nscore__list_nsmain__func__I23I 35))
(declare-const MIRNominalTypeEnum_nscore__mapentry_k_nscore__int__v_nscore__list_nsmain__func__I26I Int)
(assert (= MIRNominalTypeEnum_nscore__mapentry_k_nscore__int__v_nscore__list_nsmain__func__I26I 37))
(declare-const MIRNominalTypeEnum_nscore__noneI29I Int)
(assert (= MIRNominalTypeEnum_nscore__noneI29I 39))
(declare-const MIRNominalTypeEnum_nscore__regexI30I Int)
(assert (= MIRNominalTypeEnum_nscore__regexI30I 41))
(declare-const MIRNominalTypeEnum_nscore__stringI31I Int)
(assert (= MIRNominalTypeEnum_nscore__stringI31I 43))
(declare-const MIRNominalTypeEnum_nscore__uuidI32I Int)
(assert (= MIRNominalTypeEnum_nscore__uuidI32I 45))
(declare-const MIRNominalTypeEnum_nsmain__funcI20I Int)
(assert (= MIRNominalTypeEnum_nsmain__funcI20I 47))
(declare-const MIRNominalTypeEnum_nsmain__testschedulerI34I Int)
(assert (= MIRNominalTypeEnum_nsmain__testschedulerI34I 49))
(declare-const MIRNominalTypeEnum_nscore__anyI41I Int)
(assert (= MIRNominalTypeEnum_nscore__anyI41I 51))
(declare-const MIRNominalTypeEnum_nscore__apitypeI42I Int)
(assert (= MIRNominalTypeEnum_nscore__apitypeI42I 53))
(declare-const MIRNominalTypeEnum_nscore__apivalueI43I Int)
(assert (= MIRNominalTypeEnum_nscore__apivalueI43I 55))
(declare-const MIRNominalTypeEnum_nscore__convertableI44I Int)
(assert (= MIRNominalTypeEnum_nscore__convertableI44I 57))
(declare-const MIRNominalTypeEnum_nscore__enumI45I Int)
(assert (= MIRNominalTypeEnum_nscore__enumI45I 59))
(declare-const MIRNominalTypeEnum_nscore__expandoable_t__func_nsmain__func__time_nscore__int__I46I Int)
(assert (= MIRNominalTypeEnum_nscore__expandoable_t__func_nsmain__func__time_nscore__int__I46I 61))
(declare-const MIRNominalTypeEnum_nscore__expandoable_t_nscore__int_I47I Int)
(assert (= MIRNominalTypeEnum_nscore__expandoable_t_nscore__int_I47I 63))
(declare-const MIRNominalTypeEnum_nscore__expandoable_t_nscore__mapentry_nscore__int__nscore__list_nsmain__func___I48I Int)
(assert (= MIRNominalTypeEnum_nscore__expandoable_t_nscore__mapentry_nscore__int__nscore__list_nsmain__func___I48I 65))
(declare-const MIRNominalTypeEnum_nscore__expandoable_t_nsmain__func_I49I Int)
(assert (= MIRNominalTypeEnum_nscore__expandoable_t_nsmain__func_I49I 67))
(declare-const MIRNominalTypeEnum_nscore__idkeyI50I Int)
(assert (= MIRNominalTypeEnum_nscore__idkeyI50I 69))
(declare-const MIRNominalTypeEnum_nscore__keytypeI51I Int)
(assert (= MIRNominalTypeEnum_nscore__keytypeI51I 71))
(declare-const MIRNominalTypeEnum_nscore__objectI52I Int)
(assert (= MIRNominalTypeEnum_nscore__objectI52I 73))
(declare-const MIRNominalTypeEnum_nscore__parsableI53I Int)
(assert (= MIRNominalTypeEnum_nscore__parsableI53I 75))
(declare-const MIRNominalTypeEnum_nscore__podtypeI54I Int)
(assert (= MIRNominalTypeEnum_nscore__podtypeI54I 77))
(declare-const MIRNominalTypeEnum_nscore__recordI55I Int)
(assert (= MIRNominalTypeEnum_nscore__recordI55I 79))
(declare-const MIRNominalTypeEnum_nscore__someI56I Int)
(assert (= MIRNominalTypeEnum_nscore__someI56I 81))
(declare-const MIRNominalTypeEnum_nscore__truthyI57I Int)
(assert (= MIRNominalTypeEnum_nscore__truthyI57I 83))
(declare-const MIRNominalTypeEnum_nscore__tupleI58I Int)
(assert (= MIRNominalTypeEnum_nscore__tupleI58I 85))
(declare-const MIRNominalTypeEnum_nscore__validatorI59I Int)
(assert (= MIRNominalTypeEnum_nscore__validatorI59I 87))
(declare-const MIRNominalTypeEnum_nsmain__schedulerI60I Int)
(assert (= MIRNominalTypeEnum_nsmain__schedulerI60I 89))
(declare-const MIRNominalTypeEnum_None Int)
(declare-const MIRNominalTypeEnum_Bool Int)
(declare-const MIRNominalTypeEnum_Int Int)
(declare-const MIRNominalTypeEnum_BigInt Int)
(declare-const MIRNominalTypeEnum_Float64 Int)
(declare-const MIRNominalTypeEnum_String Int)
(declare-const MIRNominalTypeEnum_UUID Int)
(declare-const MIRNominalTypeEnum_LogicalTime Int)
(declare-const MIRNominalTypeEnum_CryptoHash Int)
(declare-const MIRNominalTypeEnum_ByteBuffer Int)
(declare-const MIRNominalTypeEnum_ISOTime Int)
(declare-const MIRNominalTypeEnum_Tuple Int)
(declare-const MIRNominalTypeEnum_Record Int)
(declare-const MIRNominalTypeEnum_Regex Int)
(assert (= MIRNominalTypeEnum_BigInt MIRNominalTypeEnum_nscore__bigintI1I))
(assert (= MIRNominalTypeEnum_Bool MIRNominalTypeEnum_nscore__boolI2I))
(assert (= MIRNominalTypeEnum_ByteBuffer MIRNominalTypeEnum_nscore__bytebufferI6I))
(assert (= MIRNominalTypeEnum_CryptoHash MIRNominalTypeEnum_nscore__cryptohashI7I))
(assert (= MIRNominalTypeEnum_Float64 MIRNominalTypeEnum_nscore__float64I8I))
(assert (= MIRNominalTypeEnum_ISOTime MIRNominalTypeEnum_nscore__isotimeI10I))
(assert (= MIRNominalTypeEnum_Int MIRNominalTypeEnum_nscore__intI9I))
(assert (= MIRNominalTypeEnum_LogicalTime MIRNominalTypeEnum_nscore__logicaltimeI22I))
(assert (= MIRNominalTypeEnum_None MIRNominalTypeEnum_nscore__noneI29I))
(assert (= MIRNominalTypeEnum_Record MIRNominalTypeEnum_nscore__recordI55I))
(assert (= MIRNominalTypeEnum_Regex MIRNominalTypeEnum_nscore__regexI30I))
(assert (= MIRNominalTypeEnum_String MIRNominalTypeEnum_nscore__stringI31I))
(assert (= MIRNominalTypeEnum_Tuple MIRNominalTypeEnum_nscore__tupleI58I))
(assert (= MIRNominalTypeEnum_UUID MIRNominalTypeEnum_nscore__uuidI32I))
(declare-fun nominalDataKinds (Int) StructuralSpecialTypeInfo)
(assert (= (nominalDataKinds MIRNominalTypeEnum_nscore__assumesafeI0I) (StructuralSpecialTypeInfo@cons false false false)))
(assert (= (nominalDataKinds MIRNominalTypeEnum_nscore__bigintI1I) (StructuralSpecialTypeInfo@cons true true true)))
(assert (= (nominalDataKinds MIRNominalTypeEnum_nscore__boolI2I) (StructuralSpecialTypeInfo@cons true true true)))
(assert (= (nominalDataKinds MIRNominalTypeEnum_nscore__buffercompressionI3I) (StructuralSpecialTypeInfo@cons true false true)))
(assert (= (nominalDataKinds MIRNominalTypeEnum_nscore__bufferencodingI4I) (StructuralSpecialTypeInfo@cons true false true)))
(assert (= (nominalDataKinds MIRNominalTypeEnum_nscore__bufferformatI5I) (StructuralSpecialTypeInfo@cons true false true)))
(assert (= (nominalDataKinds MIRNominalTypeEnum_nscore__bytebufferI6I) (StructuralSpecialTypeInfo@cons false false false)))
(assert (= (nominalDataKinds MIRNominalTypeEnum_nscore__cryptohashI7I) (StructuralSpecialTypeInfo@cons true true true)))
(assert (= (nominalDataKinds MIRNominalTypeEnum_nscore__float64I8I) (StructuralSpecialTypeInfo@cons true true true)))
(assert (= (nominalDataKinds MIRNominalTypeEnum_nscore__intI9I) (StructuralSpecialTypeInfo@cons true true true)))
(assert (= (nominalDataKinds MIRNominalTypeEnum_nscore__isotimeI10I) (StructuralSpecialTypeInfo@cons true true true)))
(assert (= (nominalDataKinds MIRNominalTypeEnum_nscore__keylist_k_nscore__int_I11I) (StructuralSpecialTypeInfo@cons false false false)))
(assert (= (nominalDataKinds MIRNominalTypeEnum_nscore__knownsafeI14I) (StructuralSpecialTypeInfo@cons false false false)))
(assert (= (nominalDataKinds MIRNominalTypeEnum_nscore__list_t__func_nsmain__func__time_nscore__int__I15I) (StructuralSpecialTypeInfo@cons false false false)))
(assert (= (nominalDataKinds MIRNominalTypeEnum_nscore__list_t_nscore__int_I17I) (StructuralSpecialTypeInfo@cons false true true)))
(assert (= (nominalDataKinds MIRNominalTypeEnum_nscore__list_t_nsmain__func_I19I) (StructuralSpecialTypeInfo@cons false false false)))
(assert (= (nominalDataKinds MIRNominalTypeEnum_nscore__logicaltimeI22I) (StructuralSpecialTypeInfo@cons true true true)))
(assert (= (nominalDataKinds MIRNominalTypeEnum_nscore__map_k_nscore__int__v_nscore__list_nsmain__func__I23I) (StructuralSpecialTypeInfo@cons false false false)))
(assert (= (nominalDataKinds MIRNominalTypeEnum_nscore__mapentry_k_nscore__int__v_nscore__list_nsmain__func__I26I) (StructuralSpecialTypeInfo@cons false false false)))
(assert (= (nominalDataKinds MIRNominalTypeEnum_nscore__noneI29I) (StructuralSpecialTypeInfo@cons true true true)))
(assert (= (nominalDataKinds MIRNominalTypeEnum_nscore__regexI30I) (StructuralSpecialTypeInfo@cons false false false)))
(assert (= (nominalDataKinds MIRNominalTypeEnum_nscore__stringI31I) (StructuralSpecialTypeInfo@cons false true true)))
(assert (= (nominalDataKinds MIRNominalTypeEnum_nscore__uuidI32I) (StructuralSpecialTypeInfo@cons true true true)))
(assert (= (nominalDataKinds MIRNominalTypeEnum_nsmain__funcI20I) (StructuralSpecialTypeInfo@cons false false false)))
(assert (= (nominalDataKinds MIRNominalTypeEnum_nsmain__testschedulerI34I) (StructuralSpecialTypeInfo@cons false false false)))
(define-fun bsqkey_get_nominal_type ((keyv BKeyValue)) Int
(ite (= keyv bsqkey_none) MIRNominalTypeEnum_None
(ite (is-bsqkey_bool keyv) MIRNominalTypeEnum_Bool
(ite (is-bsqkey_int keyv) MIRNominalTypeEnum_Int
(ite (is-bsqkey_bigint keyv) MIRNominalTypeEnum_BigInt
(ite (is-bsqkey_string keyv) MIRNominalTypeEnum_String
(ite (is-bsqkey_safestring keyv) (bsq_safestring_type (bsqkey_safestring_value keyv))
(ite (is-bsqkey_stringof keyv) (bsq_stringof_type (bsqkey_stringof_value keyv))
(ite (is-bsqkey_uuid keyv) MIRNominalTypeEnum_UUID
(ite (is-bsqkey_logicaltime keyv) MIRNominalTypeEnum_LogicalTime
(ite (is-bsqkey_cryptohash keyv) MIRNominalTypeEnum_CryptoHash
(ite (is-bsqkey_enum keyv) (bsq_enum_type (bsqkey_enum_value keyv))
(ite (is-bsqkey_idkeysimple keyv) (bsq_idkeysimple_type (bsqkey_idkeysimple_value keyv))
(bsq_idkeycompound_type (bsqkey_idkeycompound_value keyv))
)
)
)
)
)
)
)
)
)
)
)
)
)
(define-fun bsqterm_get_nominal_type ((term BTerm)) Int
(ite (is-bsqterm_float64 term) MIRNominalTypeEnum_Float64
(ite (is-bsqterm_key term) (bsqkey_get_nominal_type (bsqterm_key_value term))
(ite (is-bsqterm_buffer term) (bsq_buffer_type (bsqterm_buffer_value term))
(ite (is-bsqterm_bufferof term) (bsq_bufferof_type (bsqterm_bufferof_value term))
(ite (is-bsqterm_bytebuffer term) MIRNominalTypeEnum_ByteBuffer
(ite (is-bsqterm_isotime term) MIRNominalTypeEnum_ISOTime
(ite (is-bsqterm_regex term) MIRNominalTypeEnum_Regex
(ite (is-bsqterm_tuple term) MIRNominalTypeEnum_Tuple
(ite (is-bsqterm_record term) MIRNominalTypeEnum_Record
(bsqterm_object_type term)
)
)
)
)
)
)
)
)
)
)
(define-fun bsqkeyless_basetypes ((k1 BKeyValue) (k2 BKeyValue)) Bool
(let ((k1t (bsqkey_get_nominal_type k1)) (k2t (bsqkey_get_nominal_type k2)))
(ite (not (= k1t k2t))
(< k1t k2t)
(ite (and (= k1 bsqkey_none) (= k2 bsqkey_none)) false
(ite (and (is-bsqkey_bool k1) (is-bsqkey_bool k2)) (and (not (bsqkey_bool_value k1)) (bsqkey_bool_value k2))
(ite (and (is-bsqkey_int k1) (is-bsqkey_int k2)) (< (bsqkey_int_value k1) (bsqkey_int_value k2))
(ite (and (is-bsqkey_bigint k1) (is-bsqkey_bigint k2)) (< (bsqkey_bigint_value k1) (bsqkey_bigint_value k2))
(ite (and (is-bsqkey_string k1) (is-bsqkey_string k2)) (str.< (bsqkey_string_value k1) (bsqkey_string_value k2))
(ite (and (is-bsqkey_safestring k1) (is-bsqkey_safestring k2)) (str.< (bsq_safestring_value (bsqkey_safestring_value k1)) (bsq_safestring_value (bsqkey_safestring_value k2)))
(ite (and (is-bsqkey_stringof k1) (is-bsqkey_stringof k2)) (str.< (bsq_stringof_value (bsqkey_stringof_value k1)) (bsq_stringof_value (bsqkey_stringof_value k2)))
(ite (and (is-bsqkey_uuid k1) (is-bsqkey_uuid k2)) (str.< (bsq_uuid_value (bsqkey_uuid_value k1)) (bsq_uuid_value (bsqkey_uuid_value k2)))
(ite (and (is-bsqkey_logicaltime k1) (is-bsqkey_logicaltime k2)) (< (bsq_logicaltime_value (bsqkey_logicaltime_value k1)) (bsq_logicaltime_value (bsqkey_logicaltime_value k2)))
(ite (and (is-bsqkey_cryptohash k1) (is-bsqkey_cryptohash k2)) (str.< (bsq_cryptohash_value (bsqkey_cryptohash_value k1)) (bsq_cryptohash_value (bsqkey_cryptohash_value k2)))
(< (bsq_enum_value (bsqkey_enum_value k1)) (bsq_enum_value (bsqkey_enum_value k2)))
)
)
)
)
)
)
)
)
)
)
)
)
)
(define-fun bsqkeyless_identitysimple ((idtype Int) (k1 bsq_idkeysimple) (k2 bsq_idkeysimple)) Bool
;;
;;TODO -- need to gas bound and generate this (and bsqkeyless programatically)
;;
false
)
(define-fun bsqkeyless_identitycompound ((idtype Int) (k1 bsq_idkeycompound) (k2 bsq_idkeycompound)) Bool
;;
;;TODO -- need to gas bound and generate this (and bsqkeyless programatically)
;;
false
)
(define-fun bsqkeyless ((k1 BKeyValue) (k2 BKeyValue)) Bool
(let ((k1t (bsqkey_get_nominal_type k1)) (k2t (bsqkey_get_nominal_type k2)))
(ite (not (= k1t k2t))
(< k1t k2t)
(ite (and (is-bsqkey_idkeycompound k1) (is-bsqkey_idkeycompound k2))
(bsqkeyless_identitycompound k1t (bsqkey_idkeycompound_value k1) (bsqkey_idkeycompound_value k2))
(ite (and (is-bsqkey_idkeysimple k1) (is-bsqkey_idkeysimple k2))
(bsqkeyless_identitysimple k1t (bsqkey_idkeysimple_value k1) (bsqkey_idkeysimple_value k2))
(bsqkeyless_basetypes k1 k2)
)
)
)
)
)
(declare-const StructuralSpecialTypeInfo@Clear StructuralSpecialTypeInfo)
(assert (= StructuralSpecialTypeInfo@Clear (StructuralSpecialTypeInfo@cons true true true)))
(define-fun getStructuralSpecialTypeInfoTerm ((term BTerm)) StructuralSpecialTypeInfo
(ite (= term bsqterm@clear) StructuralSpecialTypeInfo@Clear
(ite (is-bsqterm_tuple term) (bsq_tuple_concepts (bsqterm_tuple_value term))
(ite (is-bsqterm_record term) (bsq_record_concepts (bsqterm_record_value term))
(nominalDataKinds (bsqterm_get_nominal_type term))
)
)
)
)
(define-fun mergeStructuralSpecialTypeInfo ((st1 StructuralSpecialTypeInfo) (st2 StructuralSpecialTypeInfo)) StructuralSpecialTypeInfo
(StructuralSpecialTypeInfo@cons (and (StructuralSpecialTypeInfo$PODType st1) (StructuralSpecialTypeInfo$PODType st2)) (and (StructuralSpecialTypeInfo$APIType st1) (StructuralSpecialTypeInfo$APIType st2)) (and (StructuralSpecialTypeInfo$Parsable st1) (StructuralSpecialTypeInfo$Parsable st2)))
)
(define-fun @fj ((term BTerm) (sti StructuralSpecialTypeInfo)) StructuralSpecialTypeInfo
(mergeStructuralSpecialTypeInfo (getStructuralSpecialTypeInfoTerm term) sti)
)
(declare-const @int_min Int)
(assert (= @int_min -9007199254740991))
(declare-const @int_max Int)
(assert (= @int_max 9007199254740991))
(define-fun @int_unsafe ((v Int)) Bool
(or (< v @int_min) (> v @int_max))
)
(declare-const bsqterm_none BTerm)
(assert (= bsqterm_none (bsqterm_key bsqkey_none)))
(declare-const bsqidkey_array_empty (Array Int BKeyValue))
(assert (= bsqidkey_array_empty ((as const (Array Int BKeyValue)) bsqkey_none)))
(declare-const bsqtuple_array_empty (Array Int BTerm))
(assert (= bsqtuple_array_empty ((as const (Array Int BTerm)) bsqterm@clear)))
(declare-const bsqrecord_array_empty (Array String BTerm))
(assert (= bsqrecord_array_empty ((as const (Array String BTerm)) bsqterm@clear)))
(declare-const nscore__list_t__func_nsmain__func__time_nscore__int___collection_data_array_emptyI16I (Array Int bsq_record))
(declare-const nscore__list_t_nscore__int__collection_data_array_emptyI18I (Array Int Int))
(declare-const nscore__list_t_nsmain__func__collection_data_array_emptyI21I (Array Int nsmain__funcI20I))
(declare-const nscore__map_k_nscore__int__v_nscore__list_nsmain__func___collection_data_array_emptyI24I (Array Int nscore__list_t_nsmain__func_I19I))
(declare-const nscore__map_k_nscore__int__v_nscore__list_nsmain__func___collection_has_array_emptyI25I (Array Int Bool))
(assert (= nscore__map_k_nscore__int__v_nscore__list_nsmain__func___collection_has_array_emptyI25I ((as const (Array Int Bool)) false)))
(declare-datatypes (
(ErrorCode 0)
(Result@BTerm 0)
(Result@Bool 0)
(Result@Int 0)
(Result@String 0)
(Result@bsq_record 0)
(Result@nscore__keylist_k_nscore__int_I11I 0)
(Result@nscore__list_t__func_nsmain__func__time_nscore__int__I15I 0)
(Result@nscore__list_t_nscore__int_I17I 0)
(Result@nscore__list_t_nsmain__func_I19I 0)
(Result@nsmain__funcI20I 0)
(Result@nsmain__testschedulerI34I 0)
) (
( (result_error (error_id Int)) (result_bmc (bmc_id String)) )
( (result_success@BTerm (result_success_value@BTerm BTerm)) (result_error@BTerm (result_error_code@BTerm ErrorCode)) )
( (result_success@Bool (result_success_value@Bool Bool)) (result_error@Bool (result_error_code@Bool ErrorCode)) )
( (result_success@Int (result_success_value@Int Int)) (result_error@Int (result_error_code@Int ErrorCode)) )
( (result_success@String (result_success_value@String String)) (result_error@String (result_error_code@String ErrorCode)) )
( (result_success@bsq_record (result_success_value@bsq_record bsq_record)) (result_error@bsq_record (result_error_code@bsq_record ErrorCode)) )
( (result_success@nscore__keylist_k_nscore__int_I11I (result_success_value@nscore__keylist_k_nscore__int_I11I nscore__keylist_k_nscore__int_I11I)) (result_error@nscore__keylist_k_nscore__int_I11I (result_error_code@nscore__keylist_k_nscore__int_I11I ErrorCode)) )
( (result_success@nscore__list_t__func_nsmain__func__time_nscore__int__I15I (result_success_value@nscore__list_t__func_nsmain__func__time_nscore__int__I15I nscore__list_t__func_nsmain__func__time_nscore__int__I15I)) (result_error@nscore__list_t__func_nsmain__func__time_nscore__int__I15I (result_error_code@nscore__list_t__func_nsmain__func__time_nscore__int__I15I ErrorCode)) )
( (result_success@nscore__list_t_nscore__int_I17I (result_success_value@nscore__list_t_nscore__int_I17I nscore__list_t_nscore__int_I17I)) (result_error@nscore__list_t_nscore__int_I17I (result_error_code@nscore__list_t_nscore__int_I17I ErrorCode)) )
( (result_success@nscore__list_t_nsmain__func_I19I (result_success_value@nscore__list_t_nsmain__func_I19I nscore__list_t_nsmain__func_I19I)) (result_error@nscore__list_t_nsmain__func_I19I (result_error_code@nscore__list_t_nsmain__func_I19I ErrorCode)) )
( (result_success@nsmain__funcI20I (result_success_value@nsmain__funcI20I nsmain__funcI20I)) (result_error@nsmain__funcI20I (result_error_code@nsmain__funcI20I ErrorCode)) )
( (result_success@nsmain__testschedulerI34I (result_success_value@nsmain__testschedulerI34I nsmain__testschedulerI34I)) (result_error@nsmain__testschedulerI34I (result_error_code@nsmain__testschedulerI34I ErrorCode)) )
))
(declare-const mirconceptsubtypearray_empty (Array Int Bool))
(assert (= mirconceptsubtypearray_empty ((as const (Array Int Bool)) false)))
(declare-const MIRConceptSubtypeArray$nscore__anyI41I (Array Int Bool))
(assert (= MIRConceptSubtypeArray$nscore__anyI41I (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store mirconceptsubtypearray_empty MIRNominalTypeEnum_nscore__assumesafeI0I true) MIRNominalTypeEnum_nscore__bigintI1I true) MIRNominalTypeEnum_nscore__boolI2I true) MIRNominalTypeEnum_nscore__buffercompressionI3I true) MIRNominalTypeEnum_nscore__bufferencodingI4I true) MIRNominalTypeEnum_nscore__bufferformatI5I true) MIRNominalTypeEnum_nscore__bytebufferI6I true) MIRNominalTypeEnum_nscore__cryptohashI7I true) MIRNominalTypeEnum_nscore__float64I8I true) MIRNominalTypeEnum_nscore__intI9I true) MIRNominalTypeEnum_nscore__isotimeI10I true) MIRNominalTypeEnum_nscore__keylist_k_nscore__int_I11I true) MIRNominalTypeEnum_nscore__knownsafeI14I true) MIRNominalTypeEnum_nscore__list_t__func_nsmain__func__time_nscore__int__I15I true) MIRNominalTypeEnum_nscore__list_t_nscore__int_I17I true) MIRNominalTypeEnum_nscore__list_t_nsmain__func_I19I true) MIRNominalTypeEnum_nscore__logicaltimeI22I true) MIRNominalTypeEnum_nscore__map_k_nscore__int__v_nscore__list_nsmain__func__I23I true) MIRNominalTypeEnum_nscore__mapentry_k_nscore__int__v_nscore__list_nsmain__func__I26I true) MIRNominalTypeEnum_nscore__noneI29I true) MIRNominalTypeEnum_nscore__recordI55I true) MIRNominalTypeEnum_nscore__regexI30I true) MIRNominalTypeEnum_nscore__stringI31I true) MIRNominalTypeEnum_nscore__tupleI58I true) MIRNominalTypeEnum_nscore__uuidI32I true) MIRNominalTypeEnum_nsmain__funcI20I true) MIRNominalTypeEnum_nsmain__testschedulerI34I true)))
(declare-const MIRConceptSubtypeArray$nscore__apitypeI42I (Array Int Bool))
(assert (= MIRConceptSubtypeArray$nscore__apitypeI42I (store (store (store (store (store (store (store (store (store (store (store (store (store (store mirconceptsubtypearray_empty MIRNominalTypeEnum_nscore__bigintI1I true) MIRNominalTypeEnum_nscore__boolI2I true) MIRNominalTypeEnum_nscore__buffercompressionI3I true) MIRNominalTypeEnum_nscore__bufferencodingI4I true) MIRNominalTypeEnum_nscore__bufferformatI5I true) MIRNominalTypeEnum_nscore__cryptohashI7I true) MIRNominalTypeEnum_nscore__float64I8I true) MIRNominalTypeEnum_nscore__intI9I true) MIRNominalTypeEnum_nscore__isotimeI10I true) MIRNominalTypeEnum_nscore__list_t_nscore__int_I17I true) MIRNominalTypeEnum_nscore__logicaltimeI22I true) MIRNominalTypeEnum_nscore__noneI29I true) MIRNominalTypeEnum_nscore__stringI31I true) MIRNominalTypeEnum_nscore__uuidI32I true)))
(declare-const MIRConceptSubtypeArray$nscore__apivalueI43I (Array Int Bool))
(assert (= MIRConceptSubtypeArray$nscore__apivalueI43I (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store mirconceptsubtypearray_empty MIRNominalTypeEnum_nscore__bigintI1I true) MIRNominalTypeEnum_nscore__boolI2I true) MIRNominalTypeEnum_nscore__buffercompressionI3I true) MIRNominalTypeEnum_nscore__bufferencodingI4I true) MIRNominalTypeEnum_nscore__bufferformatI5I true) MIRNominalTypeEnum_nscore__bytebufferI6I true) MIRNominalTypeEnum_nscore__cryptohashI7I true) MIRNominalTypeEnum_nscore__float64I8I true) MIRNominalTypeEnum_nscore__intI9I true) MIRNominalTypeEnum_nscore__isotimeI10I true) MIRNominalTypeEnum_nscore__list_t_nscore__int_I17I true) MIRNominalTypeEnum_nscore__logicaltimeI22I true) MIRNominalTypeEnum_nscore__noneI29I true) MIRNominalTypeEnum_nscore__stringI31I true) MIRNominalTypeEnum_nscore__uuidI32I true)))
(declare-const MIRConceptSubtypeArray$nscore__convertableI44I (Array Int Bool))
(assert (= MIRConceptSubtypeArray$nscore__convertableI44I (store mirconceptsubtypearray_empty MIRNominalTypeEnum_nscore__mapentry_k_nscore__int__v_nscore__list_nsmain__func__I26I true)))
(declare-const MIRConceptSubtypeArray$nscore__enumI45I (Array Int Bool))
(assert (= MIRConceptSubtypeArray$nscore__enumI45I (store (store (store mirconceptsubtypearray_empty MIRNominalTypeEnum_nscore__buffercompressionI3I true) MIRNominalTypeEnum_nscore__bufferencodingI4I true) MIRNominalTypeEnum_nscore__bufferformatI5I true)))
(declare-const MIRConceptSubtypeArray$nscore__expandoable_t__func_nsmain__func__time_nscore__int__I46I (Array Int Bool))
(assert (= MIRConceptSubtypeArray$nscore__expandoable_t__func_nsmain__func__time_nscore__int__I46I (store (store (store (store mirconceptsubtypearray_empty MIRNominalTypeEnum_nscore__list_t__func_nsmain__func__time_nscore__int__I15I true) MIRNominalTypeEnum_nscore__list_t_nscore__int_I17I true) MIRNominalTypeEnum_nscore__list_t_nsmain__func_I19I true) MIRNominalTypeEnum_nscore__map_k_nscore__int__v_nscore__list_nsmain__func__I23I true)))
(declare-const MIRConceptSubtypeArray$nscore__expandoable_t_nscore__int_I47I (Array Int Bool))
(assert (= MIRConceptSubtypeArray$nscore__expandoable_t_nscore__int_I47I (store (store (store (store mirconceptsubtypearray_empty MIRNominalTypeEnum_nscore__list_t__func_nsmain__func__time_nscore__int__I15I true) MIRNominalTypeEnum_nscore__list_t_nscore__int_I17I true) MIRNominalTypeEnum_nscore__list_t_nsmain__func_I19I true) MIRNominalTypeEnum_nscore__map_k_nscore__int__v_nscore__list_nsmain__func__I23I true)))
(declare-const MIRConceptSubtypeArray$nscore__expandoable_t_nscore__mapentry_nscore__int__nscore__list_nsmain__func___I48I (Array Int Bool))
(assert (= MIRConceptSubtypeArray$nscore__expandoable_t_nscore__mapentry_nscore__int__nscore__list_nsmain__func___I48I (store (store (store (store mirconceptsubtypearray_empty MIRNominalTypeEnum_nscore__list_t__func_nsmain__func__time_nscore__int__I15I true) MIRNominalTypeEnum_nscore__list_t_nscore__int_I17I true) MIRNominalTypeEnum_nscore__list_t_nsmain__func_I19I true) MIRNominalTypeEnum_nscore__map_k_nscore__int__v_nscore__list_nsmain__func__I23I true)))
(declare-const MIRConceptSubtypeArray$nscore__expandoable_t_nsmain__func_I49I (Array Int Bool))
(assert (= MIRConceptSubtypeArray$nscore__expandoable_t_nsmain__func_I49I (store (store (store (store mirconceptsubtypearray_empty MIRNominalTypeEnum_nscore__list_t__func_nsmain__func__time_nscore__int__I15I true) MIRNominalTypeEnum_nscore__list_t_nscore__int_I17I true) MIRNominalTypeEnum_nscore__list_t_nsmain__func_I19I true) MIRNominalTypeEnum_nscore__map_k_nscore__int__v_nscore__list_nsmain__func__I23I true)))
(declare-const MIRConceptSubtypeArray$nscore__keytypeI51I (Array Int Bool))
(assert (= MIRConceptSubtypeArray$nscore__keytypeI51I (store (store (store (store (store (store (store (store (store (store (store mirconceptsubtypearray_empty MIRNominalTypeEnum_nscore__bigintI1I true) MIRNominalTypeEnum_nscore__boolI2I true) MIRNominalTypeEnum_nscore__buffercompressionI3I true) MIRNominalTypeEnum_nscore__bufferencodingI4I true) MIRNominalTypeEnum_nscore__bufferformatI5I true) MIRNominalTypeEnum_nscore__cryptohashI7I true) MIRNominalTypeEnum_nscore__intI9I true) MIRNominalTypeEnum_nscore__logicaltimeI22I true) MIRNominalTypeEnum_nscore__noneI29I true) MIRNominalTypeEnum_nscore__stringI31I true) MIRNominalTypeEnum_nscore__uuidI32I true)))
(declare-const MIRConceptSubtypeArray$nscore__objectI52I (Array Int Bool))
(assert (= MIRConceptSubtypeArray$nscore__objectI52I (store (store (store (store (store (store (store mirconceptsubtypearray_empty MIRNominalTypeEnum_nscore__keylist_k_nscore__int_I11I true) MIRNominalTypeEnum_nscore__list_t__func_nsmain__func__time_nscore__int__I15I true) MIRNominalTypeEnum_nscore__list_t_nscore__int_I17I true) MIRNominalTypeEnum_nscore__list_t_nsmain__func_I19I true) MIRNominalTypeEnum_nscore__map_k_nscore__int__v_nscore__list_nsmain__func__I23I true) MIRNominalTypeEnum_nsmain__funcI20I true) MIRNominalTypeEnum_nsmain__testschedulerI34I true)))
(declare-const MIRConceptSubtypeArray$nscore__parsableI53I (Array Int Bool))
(assert (= MIRConceptSubtypeArray$nscore__parsableI53I (store (store (store (store (store (store (store (store (store (store (store (store mirconceptsubtypearray_empty MIRNominalTypeEnum_nscore__bigintI1I true) MIRNominalTypeEnum_nscore__boolI2I true) MIRNominalTypeEnum_nscore__buffercompressionI3I true) MIRNominalTypeEnum_nscore__bufferencodingI4I true) MIRNominalTypeEnum_nscore__bufferformatI5I true) MIRNominalTypeEnum_nscore__cryptohashI7I true) MIRNominalTypeEnum_nscore__float64I8I true) MIRNominalTypeEnum_nscore__intI9I true) MIRNominalTypeEnum_nscore__isotimeI10I true) MIRNominalTypeEnum_nscore__logicaltimeI22I true) MIRNominalTypeEnum_nscore__noneI29I true) MIRNominalTypeEnum_nscore__uuidI32I true)))
(declare-const MIRConceptSubtypeArray$nscore__podtypeI54I (Array Int Bool))
(assert (= MIRConceptSubtypeArray$nscore__podtypeI54I (store (store (store (store (store (store (store (store (store (store (store mirconceptsubtypearray_empty MIRNominalTypeEnum_nscore__bigintI1I true) MIRNominalTypeEnum_nscore__boolI2I true) MIRNominalTypeEnum_nscore__cryptohashI7I true) MIRNominalTypeEnum_nscore__float64I8I true) MIRNominalTypeEnum_nscore__intI9I true) MIRNominalTypeEnum_nscore__isotimeI10I true) MIRNominalTypeEnum_nscore__list_t_nscore__int_I17I true) MIRNominalTypeEnum_nscore__logicaltimeI22I true) MIRNominalTypeEnum_nscore__noneI29I true) MIRNominalTypeEnum_nscore__stringI31I true) MIRNominalTypeEnum_nscore__uuidI32I true)))
(declare-const MIRConceptSubtypeArray$nscore__recordI55I (Array Int Bool))
(assert (= MIRConceptSubtypeArray$nscore__recordI55I (store mirconceptsubtypearray_empty MIRNominalTypeEnum_nscore__recordI55I true)))
(declare-const MIRConceptSubtypeArray$nscore__someI56I (Array Int Bool))
(assert (= MIRConceptSubtypeArray$nscore__someI56I (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store mirconceptsubtypearray_empty MIRNominalTypeEnum_nscore__assumesafeI0I true) MIRNominalTypeEnum_nscore__bigintI1I true) MIRNominalTypeEnum_nscore__boolI2I true) MIRNominalTypeEnum_nscore__buffercompressionI3I true) MIRNominalTypeEnum_nscore__bufferencodingI4I true) MIRNominalTypeEnum_nscore__bufferformatI5I true) MIRNominalTypeEnum_nscore__bytebufferI6I true) MIRNominalTypeEnum_nscore__cryptohashI7I true) MIRNominalTypeEnum_nscore__float64I8I true) MIRNominalTypeEnum_nscore__intI9I true) MIRNominalTypeEnum_nscore__isotimeI10I true) MIRNominalTypeEnum_nscore__keylist_k_nscore__int_I11I true) MIRNominalTypeEnum_nscore__knownsafeI14I true) MIRNominalTypeEnum_nscore__list_t__func_nsmain__func__time_nscore__int__I15I true) MIRNominalTypeEnum_nscore__list_t_nscore__int_I17I true) MIRNominalTypeEnum_nscore__list_t_nsmain__func_I19I true) MIRNominalTypeEnum_nscore__logicaltimeI22I true) MIRNominalTypeEnum_nscore__map_k_nscore__int__v_nscore__list_nsmain__func__I23I true) MIRNominalTypeEnum_nscore__mapentry_k_nscore__int__v_nscore__list_nsmain__func__I26I true) MIRNominalTypeEnum_nscore__recordI55I true) MIRNominalTypeEnum_nscore__regexI30I true) MIRNominalTypeEnum_nscore__stringI31I true) MIRNominalTypeEnum_nscore__tupleI58I true) MIRNominalTypeEnum_nscore__uuidI32I true) MIRNominalTypeEnum_nsmain__funcI20I true) MIRNominalTypeEnum_nsmain__testschedulerI34I true)))
(declare-const MIRConceptSubtypeArray$nscore__truthyI57I (Array Int Bool))
(assert (= MIRConceptSubtypeArray$nscore__truthyI57I (store (store mirconceptsubtypearray_empty MIRNominalTypeEnum_nscore__boolI2I true) MIRNominalTypeEnum_nscore__noneI29I true)))
(declare-const MIRConceptSubtypeArray$nscore__tupleI58I (Array Int Bool))
(assert (= MIRConceptSubtypeArray$nscore__tupleI58I (store mirconceptsubtypearray_empty MIRNominalTypeEnum_nscore__tupleI58I true)))
(declare-const MIRConceptSubtypeArray$nsmain__schedulerI60I (Array Int Bool))
(assert (= MIRConceptSubtypeArray$nsmain__schedulerI60I (store mirconceptsubtypearray_empty MIRNominalTypeEnum_nsmain__testschedulerI34I true)))
(define-fun nsmain__testscheduler__newI61I () Result@bsq_record
(let ((_tmp_3I62I (nscore__map_k_nscore__int__v_nscore__list_nsmain__func__I23I@cons 0 nscore__map_k_nscore__int__v_nscore__list_nsmain__func___collection_has_array_emptyI25I nscore__map_k_nscore__int__v_nscore__list_nsmain__func___collection_data_array_emptyI24I bsqterm_none)))
(let ((_tmp_5I63I (nscore__list_t__func_nsmain__func__time_nscore__int__I15I@cons 0 nscore__list_t__func_nsmain__func__time_nscore__int___collection_data_array_emptyI16I)))
(let ((_tmp_6I64I (nscore__list_t__func_nsmain__func__time_nscore__int__I15I@cons 0 nscore__list_t__func_nsmain__func__time_nscore__int___collection_data_array_emptyI16I)))
(let ((_tmp_0I65I (bsq_record@cons (StructuralSpecialTypeInfo@cons false false false) (store (store (store (store (store (store bsqrecord_array_empty "currentTime" (bsqterm_key (bsqkey_int 0))) "now" (bsqterm_key (bsqkey_int 0))) "runlist" (bsqterm_object MIRNominalTypeEnum_nscore__list_t__func_nsmain__func__time_nscore__int__I15I (cons@bsq_object_from_nscore__list_t__func_nsmain__func__time_nscore__int__I15I _tmp_5I63I))) "running" (bsqterm_key (bsqkey_bool false))) "sortedTasks" (bsqterm_object MIRNominalTypeEnum_nscore__list_t__func_nsmain__func__time_nscore__int__I15I (cons@bsq_object_from_nscore__list_t__func_nsmain__func__time_nscore__int__I15I _tmp_6I64I))) "timeline" (bsqterm_object MIRNominalTypeEnum_nscore__map_k_nscore__int__v_nscore__list_nsmain__func__I23I (cons@bsq_object_from_nscore__map_k_nscore__int__v_nscore__list_nsmain__func__I23I _tmp_3I62I))))))
(let ((___ir_ret__I66I _tmp_0I65I))
(let (($return ___ir_ret__I66I))
(result_success@bsq_record $return)
)
)
)
)
)
))
(define-fun fn__fibersched_bsq_138__3592I67I () Result@String
(let ((___ir_ret__I66I "R1"))
(let (($return ___ir_ret__I66I))
(result_success@String $return)
)
))
(define-fun nsmain__func__enqueue_fibersched_bsq_138_0_I68I () Result@bsq_record
(let ((@tmpvar@0 fn__fibersched_bsq_138__3592I67I))
(ite (is-result_error@String @tmpvar@0)
(result_error@bsq_record (result_error_code@String @tmpvar@0))
(let ((_tmp_1I69I (result_success_value@String @tmpvar@0)))
(let ((_tmp_0I65I (bsq_record@cons (StructuralSpecialTypeInfo@cons false true true) (store bsqrecord_array_empty "lf" (bsqterm_key (bsqkey_string _tmp_1I69I))))))
(let ((___ir_ret__I66I _tmp_0I65I))
(let (($return ___ir_ret__I66I))
(result_success@bsq_record $return)
)
)
)
)
)
))
(define-fun nsmain__func___invariant_directI71I ((_lfI70I String)) Result@Bool
(let ((_tmp_0I65I (not (= _lfI70I ""))))
(let ((___ir_ret__I66I _tmp_0I65I))
(let (($return ___ir_ret__I66I))
(result_success@Bool $return)
)
)
))
(define-fun nsmain__func____invariantI72I ((_lfI70I String)) Result@Bool
(let ((_tmp_0I65I true))
(let ((@tmpvar@1 (nsmain__func___invariant_directI71I _lfI70I)))
(ite (is-result_error@Bool @tmpvar@1)
@tmpvar@1
(let ((_tmp_0_1I73I (result_success_value@Bool @tmpvar@1)))
(ite _tmp_0_1I73I
(let ((___ir_ret___1I74I _tmp_0_1I73I))
(let ((___ir_ret___2I75I ___ir_ret___1I74I))
(let (($return ___ir_ret___2I75I))
(result_success@Bool $return)
)
)
)
(let ((___ir_ret__I66I _tmp_0_1I73I))
(let ((___ir_ret___2I75I ___ir_ret__I66I))
(let (($return ___ir_ret___2I75I))
(result_success@Bool $return)
)
)
)
)
)
)
)
))
(define-fun nscore__map__s_has_key_k_nscore__int__v_nscore__list_nsmain__func__I78I ((mI76I nscore__map_k_nscore__int__v_nscore__list_nsmain__func__I23I) (keyI77I Int)) Bool
(select (nscore__map_k_nscore__int__v_nscore__list_nsmain__func__I23I@@has mI76I) keyI77I)
)
(define-fun nscore__map__has_k_nscore__int__v_nscore__list_nsmain__func__I80I ((thisI79I nscore__map_k_nscore__int__v_nscore__list_nsmain__func__I23I) (keyI77I Int)) Result@Bool
(let ((_tmp_0I65I (nscore__map__s_has_key_k_nscore__int__v_nscore__list_nsmain__func__I78I thisI79I keyI77I)))
(let ((___ir_ret__I66I _tmp_0I65I))
(let (($return ___ir_ret__I66I))
(result_success@Bool $return)
)
)
))
(define-fun nscore__list__s_size_t__func_nsmain__func__time_nscore__int__I82I ((lI81I nscore__list_t__func_nsmain__func__time_nscore__int__I15I)) Int
(nscore__list_t__func_nsmain__func__time_nscore__int__I15I@@size lI81I)
)
(define-fun nscore__list__s_unsafe_get_t__func_nsmain__func__time_nscore__int__I84I ((lI81I nscore__list_t__func_nsmain__func__time_nscore__int__I15I) (iI83I Int)) bsq_record
(select (nscore__list_t__func_nsmain__func__time_nscore__int__I15I@@entries lI81I) iI83I)
)
(define-fun fn__fibersched_bsq_71__1945I87I ((taskI85I bsq_record) (__c_atI86I Int)) Result@Bool
(let ((_tmp_3I62I (bsqkey_int_value (bsqterm_key_value (select (bsq_record_entries taskI85I) "time")))))
(let ((_tmp_0I65I (< _tmp_3I62I __c_atI86I)))
(let ((___ir_ret__I66I _tmp_0I65I))
(let (($return ___ir_ret__I66I))
(result_success@Bool $return)
)
)
)
))
(define-fun nscore__list__s_unsafe_push_t__func_nsmain__func__time_nscore__int__I89I ((lI81I nscore__list_t__func_nsmain__func__time_nscore__int__I15I) (vI88I bsq_record)) nscore__list_t__func_nsmain__func__time_nscore__int__I15I
(nscore__list_t__func_nsmain__func__time_nscore__int__I15I@cons (+ (nscore__list_t__func_nsmain__func__time_nscore__int__I15I@@size lI81I) 1) (store (nscore__list_t__func_nsmain__func__time_nscore__int__I15I@@entries lI81I) (nscore__list_t__func_nsmain__func__time_nscore__int__I15I@@size lI81I) vI88I))
)
(define-fun nscore__list__s_filter_t__func_nsmain__func__time_nscore__int___fibersched_bsq_71_0_I93I@gas1 ((lI81I nscore__list_t__func_nsmain__func__time_nscore__int__I15I) (lsizeI90I Int) (lpI91I nscore__list_t__func_nsmain__func__time_nscore__int__I15I) (idxI92I Int) (__c_atI86I Int)) Result@nscore__list_t__func_nsmain__func__time_nscore__int__I15I
(let ((_tmp_0I65I (= idxI92I lsizeI90I)))
(ite _tmp_0I65I
(let ((___ir_ret___2I75I lpI91I))
(let ((___ir_ret___3I94I ___ir_ret___2I75I))
(let (($return ___ir_ret___3I94I))
(result_success@nscore__list_t__func_nsmain__func__time_nscore__int__I15I $return)
)
)
)
(let ((_tmp_4I95I (nscore__list__s_unsafe_get_t__func_nsmain__func__time_nscore__int__I84I lI81I idxI92I)))
(let ((valI96I _tmp_4I95I))
(let ((@tmpvar@2 (fn__fibersched_bsq_71__1945I87I valI96I __c_atI86I)))
(ite (is-result_error@Bool @tmpvar@2)
(result_error@nscore__list_t__func_nsmain__func__time_nscore__int__I15I (result_error_code@Bool @tmpvar@2))
(let ((_tmp_7I97I (result_success_value@Bool @tmpvar@2)))
(ite _tmp_7I97I
(let ((_tmp_13I98I (nscore__list__s_unsafe_push_t__func_nsmain__func__time_nscore__int__I89I lpI91I valI96I)))
(let ((_tmp_16I99I (+ idxI92I 1)))
(ite (@int_unsafe _tmp_16I99I)
(result_error@nscore__list_t__func_nsmain__func__time_nscore__int__I15I (result_error 0))
(let ((@tmpvar@3 (result_error@nscore__list_t__func_nsmain__func__time_nscore__int__I15I (result_bmc "collection"))))
(ite (is-result_error@nscore__list_t__func_nsmain__func__time_nscore__int__I15I @tmpvar@3)
@tmpvar@3
(let ((_tmp_10I100I (result_success_value@nscore__list_t__func_nsmain__func__time_nscore__int__I15I @tmpvar@3)))
(let ((___ir_ret___1I74I _tmp_10I100I))
(let ((___ir_ret___3I94I ___ir_ret___1I74I))
(let (($return ___ir_ret___3I94I))
(result_success@nscore__list_t__func_nsmain__func__time_nscore__int__I15I $return)
)
)
)
)
)
)
)
)
)
(let ((_tmp_24I101I (+ idxI92I 1)))
(ite (@int_unsafe _tmp_24I101I)
(result_error@nscore__list_t__func_nsmain__func__time_nscore__int__I15I (result_error 1))
(let ((@tmpvar@4 (result_error@nscore__list_t__func_nsmain__func__time_nscore__int__I15I (result_bmc "collection"))))
(ite (is-result_error@nscore__list_t__func_nsmain__func__time_nscore__int__I15I @tmpvar@4)
@tmpvar@4
(let ((_tmp_20I102I (result_success_value@nscore__list_t__func_nsmain__func__time_nscore__int__I15I @tmpvar@4)))
(let ((___ir_ret__I66I _tmp_20I102I))
(let ((___ir_ret___3I94I ___ir_ret__I66I))
(let (($return ___ir_ret___3I94I))
(result_success@nscore__list_t__func_nsmain__func__time_nscore__int__I15I $return)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
))
(define-fun nscore__list__s_filter_t__func_nsmain__func__time_nscore__int___fibersched_bsq_71_0_I93I@gas2 ((lI81I nscore__list_t__func_nsmain__func__time_nscore__int__I15I) (lsizeI90I Int) (lpI91I nscore__list_t__func_nsmain__func__time_nscore__int__I15I) (idxI92I Int) (__c_atI86I Int)) Result@nscore__list_t__func_nsmain__func__time_nscore__int__I15I
(let ((_tmp_0I65I (= idxI92I lsizeI90I)))
(ite _tmp_0I65I
(let ((___ir_ret___2I75I lpI91I))
(let ((___ir_ret___3I94I ___ir_ret___2I75I))
(let (($return ___ir_ret___3I94I))
(result_success@nscore__list_t__func_nsmain__func__time_nscore__int__I15I $return)
)
)
)
(let ((_tmp_4I95I (nscore__list__s_unsafe_get_t__func_nsmain__func__time_nscore__int__I84I lI81I idxI92I)))
(let ((valI96I _tmp_4I95I))
(let ((@tmpvar@5 (fn__fibersched_bsq_71__1945I87I valI96I __c_atI86I)))
(ite (is-result_error@Bool @tmpvar@5)
(result_error@nscore__list_t__func_nsmain__func__time_nscore__int__I15I (result_error_code@Bool @tmpvar@5))
(let ((_tmp_7I97I (result_success_value@Bool @tmpvar@5)))
(ite _tmp_7I97I
(let ((_tmp_13I98I (nscore__list__s_unsafe_push_t__func_nsmain__func__time_nscore__int__I89I lpI91I valI96I)))
(let ((_tmp_16I99I (+ idxI92I 1)))
(ite (@int_unsafe _tmp_16I99I)
(result_error@nscore__list_t__func_nsmain__func__time_nscore__int__I15I (result_error 0))
(let ((@tmpvar@6 (nscore__list__s_filter_t__func_nsmain__func__time_nscore__int___fibersched_bsq_71_0_I93I@gas1 lI81I lsizeI90I _tmp_13I98I _tmp_16I99I __c_atI86I)))
(ite (is-result_error@nscore__list_t__func_nsmain__func__time_nscore__int__I15I @tmpvar@6)
@tmpvar@6
(let ((_tmp_10I100I (result_success_value@nscore__list_t__func_nsmain__func__time_nscore__int__I15I @tmpvar@6)))
(let ((___ir_ret___1I74I _tmp_10I100I))
(let ((___ir_ret___3I94I ___ir_ret___1I74I))
(let (($return ___ir_ret___3I94I))
(result_success@nscore__list_t__func_nsmain__func__time_nscore__int__I15I $return)
)
)
)
)
)
)
)
)
)
(let ((_tmp_24I101I (+ idxI92I 1)))
(ite (@int_unsafe _tmp_24I101I)
(result_error@nscore__list_t__func_nsmain__func__time_nscore__int__I15I (result_error 1))
(let ((@tmpvar@7 (nscore__list__s_filter_t__func_nsmain__func__time_nscore__int___fibersched_bsq_71_0_I93I@gas1 lI81I lsizeI90I lpI91I _tmp_24I101I __c_atI86I)))
(ite (is-result_error@nscore__list_t__func_nsmain__func__time_nscore__int__I15I @tmpvar@7)
@tmpvar@7
(let ((_tmp_20I102I (result_success_value@nscore__list_t__func_nsmain__func__time_nscore__int__I15I @tmpvar@7)))
(let ((___ir_ret__I66I _tmp_20I102I))
(let ((___ir_ret___3I94I ___ir_ret__I66I))
(let (($return ___ir_ret___3I94I))
(result_success@nscore__list_t__func_nsmain__func__time_nscore__int__I15I $return)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
))
(define-fun nscore__list__s_filter_t__func_nsmain__func__time_nscore__int___fibersched_bsq_71_0_I93I@gas3 ((lI81I nscore__list_t__func_nsmain__func__time_nscore__int__I15I) (lsizeI90I Int) (lpI91I nscore__list_t__func_nsmain__func__time_nscore__int__I15I) (idxI92I Int) (__c_atI86I Int)) Result@nscore__list_t__func_nsmain__func__time_nscore__int__I15I
(let ((_tmp_0I65I (= idxI92I lsizeI90I)))
(ite _tmp_0I65I
(let ((___ir_ret___2I75I lpI91I))
(let ((___ir_ret___3I94I ___ir_ret___2I75I))
(let (($return ___ir_ret___3I94I))
(result_success@nscore__list_t__func_nsmain__func__time_nscore__int__I15I $return)
)
)
)
(let ((_tmp_4I95I (nscore__list__s_unsafe_get_t__func_nsmain__func__time_nscore__int__I84I lI81I idxI92I)))
(let ((valI96I _tmp_4I95I))
(let ((@tmpvar@8 (fn__fibersched_bsq_71__1945I87I valI96I __c_atI86I)))
(ite (is-result_error@Bool @tmpvar@8)
(result_error@nscore__list_t__func_nsmain__func__time_nscore__int__I15I (result_error_code@Bool @tmpvar@8))
(let ((_tmp_7I97I (result_success_value@Bool @tmpvar@8)))
(ite _tmp_7I97I
(let ((_tmp_13I98I (nscore__list__s_unsafe_push_t__func_nsmain__func__time_nscore__int__I89I lpI91I valI96I)))
(let ((_tmp_16I99I (+ idxI92I 1)))
(ite (@int_unsafe _tmp_16I99I)
(result_error@nscore__list_t__func_nsmain__func__time_nscore__int__I15I (result_error 0))
(let ((@tmpvar@9 (nscore__list__s_filter_t__func_nsmain__func__time_nscore__int___fibersched_bsq_71_0_I93I@gas2 lI81I lsizeI90I _tmp_13I98I _tmp_16I99I __c_atI86I)))
(ite (is-result_error@nscore__list_t__func_nsmain__func__time_nscore__int__I15I @tmpvar@9)
@tmpvar@9
(let ((_tmp_10I100I (result_success_value@nscore__list_t__func_nsmain__func__time_nscore__int__I15I @tmpvar@9)))
(let ((___ir_ret___1I74I _tmp_10I100I))
(let ((___ir_ret___3I94I ___ir_ret___1I74I))
(let (($return ___ir_ret___3I94I))
(result_success@nscore__list_t__func_nsmain__func__time_nscore__int__I15I $return)
)
)
)
)
)
)
)
)
)
(let ((_tmp_24I101I (+ idxI92I 1)))
(ite (@int_unsafe _tmp_24I101I)
(result_error@nscore__list_t__func_nsmain__func__time_nscore__int__I15I (result_error 1))
(let ((@tmpvar@10 (nscore__list__s_filter_t__func_nsmain__func__time_nscore__int___fibersched_bsq_71_0_I93I@gas2 lI81I lsizeI90I lpI91I _tmp_24I101I __c_atI86I)))
(ite (is-result_error@nscore__list_t__func_nsmain__func__time_nscore__int__I15I @tmpvar@10)
@tmpvar@10
(let ((_tmp_20I102I (result_success_value@nscore__list_t__func_nsmain__func__time_nscore__int__I15I @tmpvar@10)))
(let ((___ir_ret__I66I _tmp_20I102I))
(let ((___ir_ret___3I94I ___ir_ret__I66I))
(let (($return ___ir_ret___3I94I))
(result_success@nscore__list_t__func_nsmain__func__time_nscore__int__I15I $return)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
))
(define-fun nscore__list__s_filter_t__func_nsmain__func__time_nscore__int___fibersched_bsq_71_0_I93I@gas4 ((lI81I nscore__list_t__func_nsmain__func__time_nscore__int__I15I) (lsizeI90I Int) (lpI91I nscore__list_t__func_nsmain__func__time_nscore__int__I15I) (idxI92I Int) (__c_atI86I Int)) Result@nscore__list_t__func_nsmain__func__time_nscore__int__I15I
(let ((_tmp_0I65I (= idxI92I lsizeI90I)))
(ite _tmp_0I65I
(let ((___ir_ret___2I75I lpI91I))
(let ((___ir_ret___3I94I ___ir_ret___2I75I))
(let (($return ___ir_ret___3I94I))
(result_success@nscore__list_t__func_nsmain__func__time_nscore__int__I15I $return)
)
)
)
(let ((_tmp_4I95I (nscore__list__s_unsafe_get_t__func_nsmain__func__time_nscore__int__I84I lI81I idxI92I)))
(let ((valI96I _tmp_4I95I))
(let ((@tmpvar@11 (fn__fibersched_bsq_71__1945I87I valI96I __c_atI86I)))
(ite (is-result_error@Bool @tmpvar@11)
(result_error@nscore__list_t__func_nsmain__func__time_nscore__int__I15I (result_error_code@Bool @tmpvar@11))
(let ((_tmp_7I97I (result_success_value@Bool @tmpvar@11)))
(ite _tmp_7I97I
(let ((_tmp_13I98I (nscore__list__s_unsafe_push_t__func_nsmain__func__time_nscore__int__I89I lpI91I valI96I)))
(let ((_tmp_16I99I (+ idxI92I 1)))
(ite (@int_unsafe _tmp_16I99I)
(result_error@nscore__list_t__func_nsmain__func__time_nscore__int__I15I (result_error 0))
(let ((@tmpvar@12 (nscore__list__s_filter_t__func_nsmain__func__time_nscore__int___fibersched_bsq_71_0_I93I@gas3 lI81I lsizeI90I _tmp_13I98I _tmp_16I99I __c_atI86I)))
(ite (is-result_error@nscore__list_t__func_nsmain__func__time_nscore__int__I15I @tmpvar@12)
@tmpvar@12
(let ((_tmp_10I100I (result_success_value@nscore__list_t__func_nsmain__func__time_nscore__int__I15I @tmpvar@12)))
(let ((___ir_ret___1I74I _tmp_10I100I))
(let ((___ir_ret___3I94I ___ir_ret___1I74I))
(let (($return ___ir_ret___3I94I))
(result_success@nscore__list_t__func_nsmain__func__time_nscore__int__I15I $return)
)
)
)
)
)
)
)
)
)
(let ((_tmp_24I101I (+ idxI92I 1)))
(ite (@int_unsafe _tmp_24I101I)
(result_error@nscore__list_t__func_nsmain__func__time_nscore__int__I15I (result_error 1))
(let ((@tmpvar@13 (nscore__list__s_filter_t__func_nsmain__func__time_nscore__int___fibersched_bsq_71_0_I93I@gas3 lI81I lsizeI90I lpI91I _tmp_24I101I __c_atI86I)))
(ite (is-result_error@nscore__list_t__func_nsmain__func__time_nscore__int__I15I @tmpvar@13)
@tmpvar@13
(let ((_tmp_20I102I (result_success_value@nscore__list_t__func_nsmain__func__time_nscore__int__I15I @tmpvar@13)))
(let ((___ir_ret__I66I _tmp_20I102I))
(let ((___ir_ret___3I94I ___ir_ret__I66I))
(let (($return ___ir_ret___3I94I))
(result_success@nscore__list_t__func_nsmain__func__time_nscore__int__I15I $return)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
))
(define-fun nscore__list__s_filter_t__func_nsmain__func__time_nscore__int___fibersched_bsq_71_0_I93I ((lI81I nscore__list_t__func_nsmain__func__time_nscore__int__I15I) (lsizeI90I Int) (lpI91I nscore__list_t__func_nsmain__func__time_nscore__int__I15I) (idxI92I Int) (__c_atI86I Int)) Result@nscore__list_t__func_nsmain__func__time_nscore__int__I15I
(let ((_tmp_0I65I (= idxI92I lsizeI90I)))
(ite _tmp_0I65I
(let ((___ir_ret___2I75I lpI91I))
(let ((___ir_ret___3I94I ___ir_ret___2I75I))
(let (($return ___ir_ret___3I94I))
(result_success@nscore__list_t__func_nsmain__func__time_nscore__int__I15I $return)
)
)
)
(let ((_tmp_4I95I (nscore__list__s_unsafe_get_t__func_nsmain__func__time_nscore__int__I84I lI81I idxI92I)))
(let ((valI96I _tmp_4I95I))
(let ((@tmpvar@14 (fn__fibersched_bsq_71__1945I87I valI96I __c_atI86I)))
(ite (is-result_error@Bool @tmpvar@14)
(result_error@nscore__list_t__func_nsmain__func__time_nscore__int__I15I (result_error_code@Bool @tmpvar@14))
(let ((_tmp_7I97I (result_success_value@Bool @tmpvar@14)))
(ite _tmp_7I97I
(let ((_tmp_13I98I (nscore__list__s_unsafe_push_t__func_nsmain__func__time_nscore__int__I89I lpI91I valI96I)))
(let ((_tmp_16I99I (+ idxI92I 1)))
(ite (@int_unsafe _tmp_16I99I)
(result_error@nscore__list_t__func_nsmain__func__time_nscore__int__I15I (result_error 0))
(let ((@tmpvar@15 (nscore__list__s_filter_t__func_nsmain__func__time_nscore__int___fibersched_bsq_71_0_I93I@gas4 lI81I lsizeI90I _tmp_13I98I _tmp_16I99I __c_atI86I)))
(ite (is-result_error@nscore__list_t__func_nsmain__func__time_nscore__int__I15I @tmpvar@15)
@tmpvar@15
(let ((_tmp_10I100I (result_success_value@nscore__list_t__func_nsmain__func__time_nscore__int__I15I @tmpvar@15)))
(let ((___ir_ret___1I74I _tmp_10I100I))
(let ((___ir_ret___3I94I ___ir_ret___1I74I))
(let (($return ___ir_ret___3I94I))
(result_success@nscore__list_t__func_nsmain__func__time_nscore__int__I15I $return)
)
)
)
)
)
)
)
)
)
(let ((_tmp_24I101I (+ idxI92I 1)))
(ite (@int_unsafe _tmp_24I101I)
(result_error@nscore__list_t__func_nsmain__func__time_nscore__int__I15I (result_error 1))
(let ((@tmpvar@16 (nscore__list__s_filter_t__func_nsmain__func__time_nscore__int___fibersched_bsq_71_0_I93I@gas4 lI81I lsizeI90I lpI91I _tmp_24I101I __c_atI86I)))
(ite (is-result_error@nscore__list_t__func_nsmain__func__time_nscore__int__I15I @tmpvar@16)
@tmpvar@16
(let ((_tmp_20I102I (result_success_value@nscore__list_t__func_nsmain__func__time_nscore__int__I15I @tmpvar@16)))
(let ((___ir_ret__I66I _tmp_20I102I))
(let ((___ir_ret___3I94I ___ir_ret__I66I))
(let (($return ___ir_ret___3I94I))
(result_success@nscore__list_t__func_nsmain__func__time_nscore__int__I15I $return)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
))
(define-fun nscore__list__filter_t__func_nsmain__func__time_nscore__int___fibersched_bsq_71_0_I103I ((thisI79I nscore__list_t__func_nsmain__func__time_nscore__int__I15I) (__c_atI86I Int)) Result@nscore__list_t__func_nsmain__func__time_nscore__int__I15I
(let ((_tmp_2I104I (nscore__list__s_size_t__func_nsmain__func__time_nscore__int__I82I thisI79I)))
(let ((_tmp_4I95I (nscore__list_t__func_nsmain__func__time_nscore__int__I15I@cons 0 nscore__list_t__func_nsmain__func__time_nscore__int___collection_data_array_emptyI16I)))
(let ((@tmpvar@17 (nscore__list__s_filter_t__func_nsmain__func__time_nscore__int___fibersched_bsq_71_0_I93I thisI79I _tmp_2I104I _tmp_4I95I 0 __c_atI86I)))
(ite (is-result_error@nscore__list_t__func_nsmain__func__time_nscore__int__I15I @tmpvar@17)
@tmpvar@17
(let ((_tmp_0I65I (result_success_value@nscore__list_t__func_nsmain__func__time_nscore__int__I15I @tmpvar@17)))
(let ((___ir_ret__I66I _tmp_0I65I))
(let (($return ___ir_ret__I66I))
(result_success@nscore__list_t__func_nsmain__func__time_nscore__int__I15I $return)
)
)
)
)
)
)
))
(define-fun fn__fibersched_bsq_72__2023I105I ((taskI85I bsq_record) (__c_atI86I Int)) Result@Bool
(let ((_tmp_3I62I (bsqkey_int_value (bsqterm_key_value (select (bsq_record_entries taskI85I) "time")))))
(let ((_tmp_0I65I (or (< __c_atI86I _tmp_3I62I) (= __c_atI86I _tmp_3I62I))))
(let ((___ir_ret__I66I _tmp_0I65I))
(let (($return ___ir_ret__I66I))
(result_success@Bool $return)
)
)
)
))
(define-fun nscore__list__s_filter_t__func_nsmain__func__time_nscore__int___fibersched_bsq_72_0_I106I@gas1 ((lI81I nscore__list_t__func_nsmain__func__time_nscore__int__I15I) (lsizeI90I Int) (lpI91I nscore__list_t__func_nsmain__func__time_nscore__int__I15I) (idxI92I Int) (__c_atI86I Int)) Result@nscore__list_t__func_nsmain__func__time_nscore__int__I15I
(let ((_tmp_0I65I (= idxI92I lsizeI90I)))
(ite _tmp_0I65I
(let ((___ir_ret___2I75I lpI91I))
(let ((___ir_ret___3I94I ___ir_ret___2I75I))
(let (($return ___ir_ret___3I94I))
(result_success@nscore__list_t__func_nsmain__func__time_nscore__int__I15I $return)
)
)
)
(let ((_tmp_4I95I (nscore__list__s_unsafe_get_t__func_nsmain__func__time_nscore__int__I84I lI81I idxI92I)))
(let ((valI96I _tmp_4I95I))
(let ((@tmpvar@18 (fn__fibersched_bsq_72__2023I105I valI96I __c_atI86I)))
(ite (is-result_error@Bool @tmpvar@18)
(result_error@nscore__list_t__func_nsmain__func__time_nscore__int__I15I (result_error_code@Bool @tmpvar@18))
(let ((_tmp_7I97I (result_success_value@Bool @tmpvar@18)))
(ite _tmp_7I97I
(let ((_tmp_13I98I (nscore__list__s_unsafe_push_t__func_nsmain__func__time_nscore__int__I89I lpI91I valI96I)))
(let ((_tmp_16I99I (+ idxI92I 1)))
(ite (@int_unsafe _tmp_16I99I)
(result_error@nscore__list_t__func_nsmain__func__time_nscore__int__I15I (result_error 0))
(let ((@tmpvar@19 (result_error@nscore__list_t__func_nsmain__func__time_nscore__int__I15I (result_bmc "collection"))))
(ite (is-result_error@nscore__list_t__func_nsmain__func__time_nscore__int__I15I @tmpvar@19)
@tmpvar@19
(let ((_tmp_10I100I (result_success_value@nscore__list_t__func_nsmain__func__time_nscore__int__I15I @tmpvar@19)))
(let ((___ir_ret___1I74I _tmp_10I100I))
(let ((___ir_ret___3I94I ___ir_ret___1I74I))
(let (($return ___ir_ret___3I94I))
(result_success@nscore__list_t__func_nsmain__func__time_nscore__int__I15I $return)
)
)
)
)
)
)
)
)
)
(let ((_tmp_24I101I (+ idxI92I 1)))
(ite (@int_unsafe _tmp_24I101I)
(result_error@nscore__list_t__func_nsmain__func__time_nscore__int__I15I (result_error 1))
(let ((@tmpvar@20 (result_error@nscore__list_t__func_nsmain__func__time_nscore__int__I15I (result_bmc "collection"))))
(ite (is-result_error@nscore__list_t__func_nsmain__func__time_nscore__int__I15I @tmpvar@20)
@tmpvar@20
(let ((_tmp_20I102I (result_success_value@nscore__list_t__func_nsmain__func__time_nscore__int__I15I @tmpvar@20)))
(let ((___ir_ret__I66I _tmp_20I102I))
(let ((___ir_ret___3I94I ___ir_ret__I66I))
(let (($return ___ir_ret___3I94I))
(result_success@nscore__list_t__func_nsmain__func__time_nscore__int__I15I $return)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
))
(define-fun nscore__list__s_filter_t__func_nsmain__func__time_nscore__int___fibersched_bsq_72_0_I106I@gas2 ((lI81I nscore__list_t__func_nsmain__func__time_nscore__int__I15I) (lsizeI90I Int) (lpI91I nscore__list_t__func_nsmain__func__time_nscore__int__I15I) (idxI92I Int) (__c_atI86I Int)) Result@nscore__list_t__func_nsmain__func__time_nscore__int__I15I
(let ((_tmp_0I65I (= idxI92I lsizeI90I)))
(ite _tmp_0I65I
(let ((___ir_ret___2I75I lpI91I))
(let ((___ir_ret___3I94I ___ir_ret___2I75I))
(let (($return ___ir_ret___3I94I))
(result_success@nscore__list_t__func_nsmain__func__time_nscore__int__I15I $return)
)
)
)
(let ((_tmp_4I95I (nscore__list__s_unsafe_get_t__func_nsmain__func__time_nscore__int__I84I lI81I idxI92I)))
(let ((valI96I _tmp_4I95I))
(let ((@tmpvar@21 (fn__fibersched_bsq_72__2023I105I valI96I __c_atI86I)))
(ite (is-result_error@Bool @tmpvar@21)
(result_error@nscore__list_t__func_nsmain__func__time_nscore__int__I15I (result_error_code@Bool @tmpvar@21))
(let ((_tmp_7I97I (result_success_value@Bool @tmpvar@21)))
(ite _tmp_7I97I
(let ((_tmp_13I98I (nscore__list__s_unsafe_push_t__func_nsmain__func__time_nscore__int__I89I lpI91I valI96I)))
(let ((_tmp_16I99I (+ idxI92I 1)))
(ite (@int_unsafe _tmp_16I99I)
(result_error@nscore__list_t__func_nsmain__func__time_nscore__int__I15I (result_error 0))
(let ((@tmpvar@22 (nscore__list__s_filter_t__func_nsmain__func__time_nscore__int___fibersched_bsq_72_0_I106I@gas1 lI81I lsizeI90I _tmp_13I98I _tmp_16I99I __c_atI86I)))
(ite (is-result_error@nscore__list_t__func_nsmain__func__time_nscore__int__I15I @tmpvar@22)
@tmpvar@22
(let ((_tmp_10I100I (result_success_value@nscore__list_t__func_nsmain__func__time_nscore__int__I15I @tmpvar@22)))
(let ((___ir_ret___1I74I _tmp_10I100I))
(let ((___ir_ret___3I94I ___ir_ret___1I74I))
(let (($return ___ir_ret___3I94I))
(result_success@nscore__list_t__func_nsmain__func__time_nscore__int__I15I $return)
)
)
)
)
)
)
)
)
)
(let ((_tmp_24I101I (+ idxI92I 1)))
(ite (@int_unsafe _tmp_24I101I)
(result_error@nscore__list_t__func_nsmain__func__time_nscore__int__I15I (result_error 1))
(let ((@tmpvar@23 (nscore__list__s_filter_t__func_nsmain__func__time_nscore__int___fibersched_bsq_72_0_I106I@gas1 lI81I lsizeI90I lpI91I _tmp_24I101I __c_atI86I)))
(ite (is-result_error@nscore__list_t__func_nsmain__func__time_nscore__int__I15I @tmpvar@23)
@tmpvar@23
(let ((_tmp_20I102I (result_success_value@nscore__list_t__func_nsmain__func__time_nscore__int__I15I @tmpvar@23)))
(let ((___ir_ret__I66I _tmp_20I102I))
(let ((___ir_ret___3I94I ___ir_ret__I66I))
(let (($return ___ir_ret___3I94I))
(result_success@nscore__list_t__func_nsmain__func__time_nscore__int__I15I $return)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
))
(define-fun nscore__list__s_filter_t__func_nsmain__func__time_nscore__int___fibersched_bsq_72_0_I106I@gas3 ((lI81I nscore__list_t__func_nsmain__func__time_nscore__int__I15I) (lsizeI90I Int) (lpI91I nscore__list_t__func_nsmain__func__time_nscore__int__I15I) (idxI92I Int) (__c_atI86I Int)) Result@nscore__list_t__func_nsmain__func__time_nscore__int__I15I
(let ((_tmp_0I65I (= idxI92I lsizeI90I)))
(ite _tmp_0I65I
(let ((___ir_ret___2I75I lpI91I))
(let ((___ir_ret___3I94I ___ir_ret___2I75I))
(let (($return ___ir_ret___3I94I))
(result_success@nscore__list_t__func_nsmain__func__time_nscore__int__I15I $return)
)
)
)
(let ((_tmp_4I95I (nscore__list__s_unsafe_get_t__func_nsmain__func__time_nscore__int__I84I lI81I idxI92I)))
(let ((valI96I _tmp_4I95I))
(let ((@tmpvar@24 (fn__fibersched_bsq_72__2023I105I valI96I __c_atI86I)))
(ite (is-result_error@Bool @tmpvar@24)
(result_error@nscore__list_t__func_nsmain__func__time_nscore__int__I15I (result_error_code@Bool @tmpvar@24))
(let ((_tmp_7I97I (result_success_value@Bool @tmpvar@24)))
(ite _tmp_7I97I
(let ((_tmp_13I98I (nscore__list__s_unsafe_push_t__func_nsmain__func__time_nscore__int__I89I lpI91I valI96I)))
(let ((_tmp_16I99I (+ idxI92I 1)))
(ite (@int_unsafe _tmp_16I99I)
(result_error@nscore__list_t__func_nsmain__func__time_nscore__int__I15I (result_error 0))
(let ((@tmpvar@25 (nscore__list__s_filter_t__func_nsmain__func__time_nscore__int___fibersched_bsq_72_0_I106I@gas2 lI81I lsizeI90I _tmp_13I98I _tmp_16I99I __c_atI86I)))
(ite (is-result_error@nscore__list_t__func_nsmain__func__time_nscore__int__I15I @tmpvar@25)
@tmpvar@25
(let ((_tmp_10I100I (result_success_value@nscore__list_t__func_nsmain__func__time_nscore__int__I15I @tmpvar@25)))
(let ((___ir_ret___1I74I _tmp_10I100I))
(let ((___ir_ret___3I94I ___ir_ret___1I74I))
(let (($return ___ir_ret___3I94I))
(result_success@nscore__list_t__func_nsmain__func__time_nscore__int__I15I $return)
)
)
)
)
)
)
)
)
)
(let ((_tmp_24I101I (+ idxI92I 1)))
(ite (@int_unsafe _tmp_24I101I)
(result_error@nscore__list_t__func_nsmain__func__time_nscore__int__I15I (result_error 1))
(let ((@tmpvar@26 (nscore__list__s_filter_t__func_nsmain__func__time_nscore__int___fibersched_bsq_72_0_I106I@gas2 lI81I lsizeI90I lpI91I _tmp_24I101I __c_atI86I)))
(ite (is-result_error@nscore__list_t__func_nsmain__func__time_nscore__int__I15I @tmpvar@26)
@tmpvar@26
(let ((_tmp_20I102I (result_success_value@nscore__list_t__func_nsmain__func__time_nscore__int__I15I @tmpvar@26)))
(let ((___ir_ret__I66I _tmp_20I102I))
(let ((___ir_ret___3I94I ___ir_ret__I66I))
(let (($return ___ir_ret___3I94I))
(result_success@nscore__list_t__func_nsmain__func__time_nscore__int__I15I $return)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
))
(define-fun nscore__list__s_filter_t__func_nsmain__func__time_nscore__int___fibersched_bsq_72_0_I106I@gas4 ((lI81I nscore__list_t__func_nsmain__func__time_nscore__int__I15I) (lsizeI90I Int) (lpI91I nscore__list_t__func_nsmain__func__time_nscore__int__I15I) (idxI92I Int) (__c_atI86I Int)) Result@nscore__list_t__func_nsmain__func__time_nscore__int__I15I
(let ((_tmp_0I65I (= idxI92I lsizeI90I)))
(ite _tmp_0I65I
(let ((___ir_ret___2I75I lpI91I))
(let ((___ir_ret___3I94I ___ir_ret___2I75I))
(let (($return ___ir_ret___3I94I))
(result_success@nscore__list_t__func_nsmain__func__time_nscore__int__I15I $return)
)
)
)
(let ((_tmp_4I95I (nscore__list__s_unsafe_get_t__func_nsmain__func__time_nscore__int__I84I lI81I idxI92I)))
(let ((valI96I _tmp_4I95I))
(let ((@tmpvar@27 (fn__fibersched_bsq_72__2023I105I valI96I __c_atI86I)))
(ite (is-result_error@Bool @tmpvar@27)
(result_error@nscore__list_t__func_nsmain__func__time_nscore__int__I15I (result_error_code@Bool @tmpvar@27))
(let ((_tmp_7I97I (result_success_value@Bool @tmpvar@27)))
(ite _tmp_7I97I
(let ((_tmp_13I98I (nscore__list__s_unsafe_push_t__func_nsmain__func__time_nscore__int__I89I lpI91I valI96I)))
(let ((_tmp_16I99I (+ idxI92I 1)))
(ite (@int_unsafe _tmp_16I99I)
(result_error@nscore__list_t__func_nsmain__func__time_nscore__int__I15I (result_error 0))
(let ((@tmpvar@28 (nscore__list__s_filter_t__func_nsmain__func__time_nscore__int___fibersched_bsq_72_0_I106I@gas3 lI81I lsizeI90I _tmp_13I98I _tmp_16I99I __c_atI86I)))
(ite (is-result_error@nscore__list_t__func_nsmain__func__time_nscore__int__I15I @tmpvar@28)
@tmpvar@28
(let ((_tmp_10I100I (result_success_value@nscore__list_t__func_nsmain__func__time_nscore__int__I15I @tmpvar@28)))
(let ((___ir_ret___1I74I _tmp_10I100I))
(let ((___ir_ret___3I94I ___ir_ret___1I74I))
(let (($return ___ir_ret___3I94I))
(result_success@nscore__list_t__func_nsmain__func__time_nscore__int__I15I $return)
)
)
)
)
)
)
)
)
)
(let ((_tmp_24I101I (+ idxI92I 1)))
(ite (@int_unsafe _tmp_24I101I)
(result_error@nscore__list_t__func_nsmain__func__time_nscore__int__I15I (result_error 1))
(let ((@tmpvar@29 (nscore__list__s_filter_t__func_nsmain__func__time_nscore__int___fibersched_bsq_72_0_I106I@gas3 lI81I lsizeI90I lpI91I _tmp_24I101I __c_atI86I)))
(ite (is-result_error@nscore__list_t__func_nsmain__func__time_nscore__int__I15I @tmpvar@29)
@tmpvar@29
(let ((_tmp_20I102I (result_success_value@nscore__list_t__func_nsmain__func__time_nscore__int__I15I @tmpvar@29)))
(let ((___ir_ret__I66I _tmp_20I102I))
(let ((___ir_ret___3I94I ___ir_ret__I66I))
(let (($return ___ir_ret___3I94I))
(result_success@nscore__list_t__func_nsmain__func__time_nscore__int__I15I $return)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
))
(define-fun nscore__list__s_filter_t__func_nsmain__func__time_nscore__int___fibersched_bsq_72_0_I106I ((lI81I nscore__list_t__func_nsmain__func__time_nscore__int__I15I) (lsizeI90I Int) (lpI91I nscore__list_t__func_nsmain__func__time_nscore__int__I15I) (idxI92I Int) (__c_atI86I Int)) Result@nscore__list_t__func_nsmain__func__time_nscore__int__I15I
(let ((_tmp_0I65I (= idxI92I lsizeI90I)))
(ite _tmp_0I65I
(let ((___ir_ret___2I75I lpI91I))
(let ((___ir_ret___3I94I ___ir_ret___2I75I))
(let (($return ___ir_ret___3I94I))
(result_success@nscore__list_t__func_nsmain__func__time_nscore__int__I15I $return)
)
)
)
(let ((_tmp_4I95I (nscore__list__s_unsafe_get_t__func_nsmain__func__time_nscore__int__I84I lI81I idxI92I)))
(let ((valI96I _tmp_4I95I))
(let ((@tmpvar@30 (fn__fibersched_bsq_72__2023I105I valI96I __c_atI86I)))
(ite (is-result_error@Bool @tmpvar@30)
(result_error@nscore__list_t__func_nsmain__func__time_nscore__int__I15I (result_error_code@Bool @tmpvar@30))
(let ((_tmp_7I97I (result_success_value@Bool @tmpvar@30)))
(ite _tmp_7I97I
(let ((_tmp_13I98I (nscore__list__s_unsafe_push_t__func_nsmain__func__time_nscore__int__I89I lpI91I valI96I)))
(let ((_tmp_16I99I (+ idxI92I 1)))
(ite (@int_unsafe _tmp_16I99I)
(result_error@nscore__list_t__func_nsmain__func__time_nscore__int__I15I (result_error 0))
(let ((@tmpvar@31 (nscore__list__s_filter_t__func_nsmain__func__time_nscore__int___fibersched_bsq_72_0_I106I@gas4 lI81I lsizeI90I _tmp_13I98I _tmp_16I99I __c_atI86I)))
(ite (is-result_error@nscore__list_t__func_nsmain__func__time_nscore__int__I15I @tmpvar@31)
@tmpvar@31
(let ((_tmp_10I100I (result_success_value@nscore__list_t__func_nsmain__func__time_nscore__int__I15I @tmpvar@31)))
(let ((___ir_ret___1I74I _tmp_10I100I))
(let ((___ir_ret___3I94I ___ir_ret___1I74I))
(let (($return ___ir_ret___3I94I))
(result_success@nscore__list_t__func_nsmain__func__time_nscore__int__I15I $return)
)
)
)
)
)
)
)
)
)
(let ((_tmp_24I101I (+ idxI92I 1)))
(ite (@int_unsafe _tmp_24I101I)
(result_error@nscore__list_t__func_nsmain__func__time_nscore__int__I15I (result_error 1))
(let ((@tmpvar@32 (nscore__list__s_filter_t__func_nsmain__func__time_nscore__int___fibersched_bsq_72_0_I106I@gas4 lI81I lsizeI90I lpI91I _tmp_24I101I __c_atI86I)))
(ite (is-result_error@nscore__list_t__func_nsmain__func__time_nscore__int__I15I @tmpvar@32)
@tmpvar@32
(let ((_tmp_20I102I (result_success_value@nscore__list_t__func_nsmain__func__time_nscore__int__I15I @tmpvar@32)))
(let ((___ir_ret__I66I _tmp_20I102I))
(let ((___ir_ret___3I94I ___ir_ret__I66I))
(let (($return ___ir_ret___3I94I))
(result_success@nscore__list_t__func_nsmain__func__time_nscore__int__I15I $return)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
))
(define-fun nscore__list__filter_t__func_nsmain__func__time_nscore__int___fibersched_bsq_72_0_I107I ((thisI79I nscore__list_t__func_nsmain__func__time_nscore__int__I15I) (__c_atI86I Int)) Result@nscore__list_t__func_nsmain__func__time_nscore__int__I15I
(let ((_tmp_2I104I (nscore__list__s_size_t__func_nsmain__func__time_nscore__int__I82I thisI79I)))
(let ((_tmp_4I95I (nscore__list_t__func_nsmain__func__time_nscore__int__I15I@cons 0 nscore__list_t__func_nsmain__func__time_nscore__int___collection_data_array_emptyI16I)))
(let ((@tmpvar@33 (nscore__list__s_filter_t__func_nsmain__func__time_nscore__int___fibersched_bsq_72_0_I106I thisI79I _tmp_2I104I _tmp_4I95I 0 __c_atI86I)))
(ite (is-result_error@nscore__list_t__func_nsmain__func__time_nscore__int__I15I @tmpvar@33)
@tmpvar@33
(let ((_tmp_0I65I (result_success_value@nscore__list_t__func_nsmain__func__time_nscore__int__I15I @tmpvar@33)))
(let ((___ir_ret__I66I _tmp_0I65I))
(let (($return ___ir_ret__I66I))
(result_success@nscore__list_t__func_nsmain__func__time_nscore__int__I15I $return)
)
)
)
)
)
)
))
(define-fun nscore__list__s_append_t__func_nsmain__func__time_nscore__int__I108I@gas1 ((lI81I nscore__list_t__func_nsmain__func__time_nscore__int__I15I) (lsizeI90I Int) (lpI91I nscore__list_t__func_nsmain__func__time_nscore__int__I15I) (idxI92I Int)) Result@nscore__list_t__func_nsmain__func__time_nscore__int__I15I
(let ((_tmp_0I65I (= idxI92I lsizeI90I)))
(ite _tmp_0I65I
(let ((___ir_ret___1I74I lpI91I))
(let ((___ir_ret___2I75I ___ir_ret___1I74I))
(let (($return ___ir_ret___2I75I))
(result_success@nscore__list_t__func_nsmain__func__time_nscore__int__I15I $return)
)
)
)
(let ((_tmp_4I95I (nscore__list__s_unsafe_get_t__func_nsmain__func__time_nscore__int__I84I lI81I idxI92I)))
(let ((valI96I _tmp_4I95I))
(let ((_tmp_10I100I (nscore__list__s_unsafe_push_t__func_nsmain__func__time_nscore__int__I89I lpI91I valI96I)))
(let ((_tmp_13I98I (+ idxI92I 1)))
(ite (@int_unsafe _tmp_13I98I)
(result_error@nscore__list_t__func_nsmain__func__time_nscore__int__I15I (result_error 2))
(let ((@tmpvar@34 (result_error@nscore__list_t__func_nsmain__func__time_nscore__int__I15I (result_bmc "collection"))))
(ite (is-result_error@nscore__list_t__func_nsmain__func__time_nscore__int__I15I @tmpvar@34)
@tmpvar@34
(let ((_tmp_7I97I (result_success_value@nscore__list_t__func_nsmain__func__time_nscore__int__I15I @tmpvar@34)))
(let ((___ir_ret__I66I _tmp_7I97I))
(let ((___ir_ret___2I75I ___ir_ret__I66I))
(let (($return ___ir_ret___2I75I))
(result_success@nscore__list_t__func_nsmain__func__time_nscore__int__I15I $return)
)
)
)
)
)
)
)
)
)
)
)
)
))
(define-fun nscore__list__s_append_t__func_nsmain__func__time_nscore__int__I108I@gas2 ((lI81I nscore__list_t__func_nsmain__func__time_nscore__int__I15I) (lsizeI90I Int) (lpI91I nscore__list_t__func_nsmain__func__time_nscore__int__I15I) (idxI92I Int)) Result@nscore__list_t__func_nsmain__func__time_nscore__int__I15I
(let ((_tmp_0I65I (= idxI92I lsizeI90I)))
(ite _tmp_0I65I
(let ((___ir_ret___1I74I lpI91I))
(let ((___ir_ret___2I75I ___ir_ret___1I74I))
(let (($return ___ir_ret___2I75I))
(result_success@nscore__list_t__func_nsmain__func__time_nscore__int__I15I $return)
)
)
)
(let ((_tmp_4I95I (nscore__list__s_unsafe_get_t__func_nsmain__func__time_nscore__int__I84I lI81I idxI92I)))
(let ((valI96I _tmp_4I95I))
(let ((_tmp_10I100I (nscore__list__s_unsafe_push_t__func_nsmain__func__time_nscore__int__I89I lpI91I valI96I)))
(let ((_tmp_13I98I (+ idxI92I 1)))
(ite (@int_unsafe _tmp_13I98I)
(result_error@nscore__list_t__func_nsmain__func__time_nscore__int__I15I (result_error 2))
(let ((@tmpvar@35 (nscore__list__s_append_t__func_nsmain__func__time_nscore__int__I108I@gas1 lI81I lsizeI90I _tmp_10I100I _tmp_13I98I)))
(ite (is-result_error@nscore__list_t__func_nsmain__func__time_nscore__int__I15I @tmpvar@35)
@tmpvar@35
(let ((_tmp_7I97I (result_success_value@nscore__list_t__func_nsmain__func__time_nscore__int__I15I @tmpvar@35)))
(let ((___ir_ret__I66I _tmp_7I97I))
(let ((___ir_ret___2I75I ___ir_ret__I66I))
(let (($return ___ir_ret___2I75I))
(result_success@nscore__list_t__func_nsmain__func__time_nscore__int__I15I $return)
)
)
)
)
)
)
)
)
)
)
)
)
))
(define-fun nscore__list__s_append_t__func_nsmain__func__time_nscore__int__I108I@gas3 ((lI81I nscore__list_t__func_nsmain__func__time_nscore__int__I15I) (lsizeI90I Int) (lpI91I nscore__list_t__func_nsmain__func__time_nscore__int__I15I) (idxI92I Int)) Result@nscore__list_t__func_nsmain__func__time_nscore__int__I15I
(let ((_tmp_0I65I (= idxI92I lsizeI90I)))
(ite _tmp_0I65I
(let ((___ir_ret___1I74I lpI91I))
(let ((___ir_ret___2I75I ___ir_ret___1I74I))
(let (($return ___ir_ret___2I75I))
(result_success@nscore__list_t__func_nsmain__func__time_nscore__int__I15I $return)
)
)
)
(let ((_tmp_4I95I (nscore__list__s_unsafe_get_t__func_nsmain__func__time_nscore__int__I84I lI81I idxI92I)))
(let ((valI96I _tmp_4I95I))
(let ((_tmp_10I100I (nscore__list__s_unsafe_push_t__func_nsmain__func__time_nscore__int__I89I lpI91I valI96I)))
(let ((_tmp_13I98I (+ idxI92I 1)))
(ite (@int_unsafe _tmp_13I98I)
(result_error@nscore__list_t__func_nsmain__func__time_nscore__int__I15I (result_error 2))
(let ((@tmpvar@36 (nscore__list__s_append_t__func_nsmain__func__time_nscore__int__I108I@gas2 lI81I lsizeI90I _tmp_10I100I _tmp_13I98I)))
(ite (is-result_error@nscore__list_t__func_nsmain__func__time_nscore__int__I15I @tmpvar@36)
@tmpvar@36
(let ((_tmp_7I97I (result_success_value@nscore__list_t__func_nsmain__func__time_nscore__int__I15I @tmpvar@36)))
(let ((___ir_ret__I66I _tmp_7I97I))
(let ((___ir_ret___2I75I ___ir_ret__I66I))
(let (($return ___ir_ret___2I75I))
(result_success@nscore__list_t__func_nsmain__func__time_nscore__int__I15I $return)
)
)
)
)
)
)
)
)
)
)
)
)
))
(define-fun nscore__list__s_append_t__func_nsmain__func__time_nscore__int__I108I@gas4 ((lI81I nscore__list_t__func_nsmain__func__time_nscore__int__I15I) (lsizeI90I Int) (lpI91I nscore__list_t__func_nsmain__func__time_nscore__int__I15I) (idxI92I Int)) Result@nscore__list_t__func_nsmain__func__time_nscore__int__I15I
(let ((_tmp_0I65I (= idxI92I lsizeI90I)))
(ite _tmp_0I65I
(let ((___ir_ret___1I74I lpI91I))
(let ((___ir_ret___2I75I ___ir_ret___1I74I))
(let (($return ___ir_ret___2I75I))
(result_success@nscore__list_t__func_nsmain__func__time_nscore__int__I15I $return)
)
)
)
(let ((_tmp_4I95I (nscore__list__s_unsafe_get_t__func_nsmain__func__time_nscore__int__I84I lI81I idxI92I)))
(let ((valI96I _tmp_4I95I))
(let ((_tmp_10I100I (nscore__list__s_unsafe_push_t__func_nsmain__func__time_nscore__int__I89I lpI91I valI96I)))
(let ((_tmp_13I98I (+ idxI92I 1)))
(ite (@int_unsafe _tmp_13I98I)
(result_error@nscore__list_t__func_nsmain__func__time_nscore__int__I15I (result_error 2))
(let ((@tmpvar@37 (nscore__list__s_append_t__func_nsmain__func__time_nscore__int__I108I@gas3 lI81I lsizeI90I _tmp_10I100I _tmp_13I98I)))
(ite (is-result_error@nscore__list_t__func_nsmain__func__time_nscore__int__I15I @tmpvar@37)
@tmpvar@37
(let ((_tmp_7I97I (result_success_value@nscore__list_t__func_nsmain__func__time_nscore__int__I15I @tmpvar@37)))
(let ((___ir_ret__I66I _tmp_7I97I))
(let ((___ir_ret___2I75I ___ir_ret__I66I))
(let (($return ___ir_ret___2I75I))
(result_success@nscore__list_t__func_nsmain__func__time_nscore__int__I15I $return)
)
)
)
)
)
)
)
)
)
)
)
)
))
(define-fun nscore__list__s_append_t__func_nsmain__func__time_nscore__int__I108I ((lI81I nscore__list_t__func_nsmain__func__time_nscore__int__I15I) (lsizeI90I Int) (lpI91I nscore__list_t__func_nsmain__func__time_nscore__int__I15I) (idxI92I Int)) Result@nscore__list_t__func_nsmain__func__time_nscore__int__I15I
(let ((_tmp_0I65I (= idxI92I lsizeI90I)))
(ite _tmp_0I65I
(let ((___ir_ret___1I74I lpI91I))
(let ((___ir_ret___2I75I ___ir_ret___1I74I))
(let (($return ___ir_ret___2I75I))
(result_success@nscore__list_t__func_nsmain__func__time_nscore__int__I15I $return)
)
)
)
(let ((_tmp_4I95I (nscore__list__s_unsafe_get_t__func_nsmain__func__time_nscore__int__I84I lI81I idxI92I)))
(let ((valI96I _tmp_4I95I))
(let ((_tmp_10I100I (nscore__list__s_unsafe_push_t__func_nsmain__func__time_nscore__int__I89I lpI91I valI96I)))
(let ((_tmp_13I98I (+ idxI92I 1)))
(ite (@int_unsafe _tmp_13I98I)
(result_error@nscore__list_t__func_nsmain__func__time_nscore__int__I15I (result_error 2))
(let ((@tmpvar@38 (nscore__list__s_append_t__func_nsmain__func__time_nscore__int__I108I@gas4 lI81I lsizeI90I _tmp_10I100I _tmp_13I98I)))
(ite (is-result_error@nscore__list_t__func_nsmain__func__time_nscore__int__I15I @tmpvar@38)
@tmpvar@38
(let ((_tmp_7I97I (result_success_value@nscore__list_t__func_nsmain__func__time_nscore__int__I15I @tmpvar@38)))
(let ((___ir_ret__I66I _tmp_7I97I))
(let ((___ir_ret___2I75I ___ir_ret__I66I))
(let (($return ___ir_ret___2I75I))
(result_success@nscore__list_t__func_nsmain__func__time_nscore__int__I15I $return)
)
)
)
)
)
)
)
)
)
)
)
)
))
(define-fun nscore__list__append_t__func_nsmain__func__time_nscore__int__I109I ((thisI79I nscore__list_t__func_nsmain__func__time_nscore__int__I15I) (lI81I nscore__list_t__func_nsmain__func__time_nscore__int__I15I)) Result@nscore__list_t__func_nsmain__func__time_nscore__int__I15I
(let ((_tmp_2I104I (nscore__list__s_size_t__func_nsmain__func__time_nscore__int__I82I lI81I)))
(let ((@tmpvar@39 (nscore__list__s_append_t__func_nsmain__func__time_nscore__int__I108I lI81I _tmp_2I104I thisI79I 0)))
(ite (is-result_error@nscore__list_t__func_nsmain__func__time_nscore__int__I15I @tmpvar@39)
@tmpvar@39
(let ((_tmp_0I65I (result_success_value@nscore__list_t__func_nsmain__func__time_nscore__int__I15I @tmpvar@39)))
(let ((___ir_ret__I66I _tmp_0I65I))
(let (($return ___ir_ret__I66I))
(result_success@nscore__list_t__func_nsmain__func__time_nscore__int__I15I $return)
)
)
)
)
)
))
(define-fun nsmain__testscheduler__usched__lselect_done_3I113I ((atI110I Int) (funcI111I nsmain__funcI20I) (thisI79I nsmain__testschedulerI34I) (_tmp_5_2I112I nscore__map_k_nscore__int__v_nscore__list_nsmain__func__I23I)) Result@nsmain__testschedulerI34I
(let ((updatedtimelineI114I _tmp_5_2I112I))
(let ((_tmp_32I115I (nsmain__testschedulerI34I@nsmain__testscheduler_sortedtasksI40I thisI79I)))
(let ((@tmpvar@40 (nscore__list__filter_t__func_nsmain__func__time_nscore__int___fibersched_bsq_71_0_I103I _tmp_32I115I atI110I)))
(ite (is-result_error@nscore__list_t__func_nsmain__func__time_nscore__int__I15I @tmpvar@40)
(result_error@nsmain__testschedulerI34I (result_error_code@nscore__list_t__func_nsmain__func__time_nscore__int__I15I @tmpvar@40))
(let ((_tmp_33I116I (result_success_value@nscore__list_t__func_nsmain__func__time_nscore__int__I15I @tmpvar@40)))
(let ((tasksbeforeI117I _tmp_33I116I))
(let ((_tmp_37I118I (nsmain__testschedulerI34I@nsmain__testscheduler_sortedtasksI40I thisI79I)))
(let ((@tmpvar@41 (nscore__list__filter_t__func_nsmain__func__time_nscore__int___fibersched_bsq_72_0_I107I _tmp_37I118I atI110I)))
(ite (is-result_error@nscore__list_t__func_nsmain__func__time_nscore__int__I15I @tmpvar@41)
(result_error@nsmain__testschedulerI34I (result_error_code@nscore__list_t__func_nsmain__func__time_nscore__int__I15I @tmpvar@41))
(let ((_tmp_38I119I (result_success_value@nscore__list_t__func_nsmain__func__time_nscore__int__I15I @tmpvar@41)))
(let ((tasksafterI120I _tmp_38I119I))
(let ((_tmp_47I121I (bsq_record@cons (StructuralSpecialTypeInfo@cons false false false) (store (store bsqrecord_array_empty "func" (bsqterm_object MIRNominalTypeEnum_nsmain__funcI20I (cons@bsq_object_from_nsmain__funcI20I funcI111I))) "time" (bsqterm_key (bsqkey_int atI110I))))))
(let ((_tmp_46I122I (nscore__list_t__func_nsmain__func__time_nscore__int__I15I@cons 1 (store nscore__list_t__func_nsmain__func__time_nscore__int___collection_data_array_emptyI16I 0 _tmp_47I121I))))
(let ((@tmpvar@42 (nscore__list__append_t__func_nsmain__func__time_nscore__int__I109I tasksbeforeI117I _tmp_46I122I)))
(ite (is-result_error@nscore__list_t__func_nsmain__func__time_nscore__int__I15I @tmpvar@42)
(result_error@nsmain__testschedulerI34I (result_error_code@nscore__list_t__func_nsmain__func__time_nscore__int__I15I @tmpvar@42))
(let ((_tmp_45I123I (result_success_value@nscore__list_t__func_nsmain__func__time_nscore__int__I15I @tmpvar@42)))
(let ((@tmpvar@43 (nscore__list__append_t__func_nsmain__func__time_nscore__int__I109I _tmp_45I123I tasksafterI120I)))
(ite (is-result_error@nscore__list_t__func_nsmain__func__time_nscore__int__I15I @tmpvar@43)
(result_error@nsmain__testschedulerI34I (result_error_code@nscore__list_t__func_nsmain__func__time_nscore__int__I15I @tmpvar@43))
(let ((_tmp_50I124I (result_success_value@nscore__list_t__func_nsmain__func__time_nscore__int__I15I @tmpvar@43)))
(let ((_tmp_42I125I (nsmain__testschedulerI34I@cons (nsmain__testschedulerI34I@nsmain__testscheduler_nowI35I thisI79I) (nsmain__testschedulerI34I@nsmain__testscheduler_currenttimeI36I thisI79I) updatedtimelineI114I (nsmain__testschedulerI34I@nsmain__testscheduler_runningI38I thisI79I) (nsmain__testschedulerI34I@nsmain__testscheduler_runlistI39I thisI79I) _tmp_50I124I)))
(let ((___ir_ret__I66I _tmp_42I125I))
(let (($return ___ir_ret__I66I))
(result_success@nsmain__testschedulerI34I $return)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
))
(define-fun nscore__map__s_get_keylist_k_nscore__int__v_nscore__list_nsmain__func__I126I ((mI76I nscore__map_k_nscore__int__v_nscore__list_nsmain__func__I23I)) BTerm
(nscore__map_k_nscore__int__v_nscore__list_nsmain__func__I23I@@keylist mI76I)
)
(define-fun nscore__keylist__s_insert_k_nscore__int_I128I@gas1 ((klI127I nscore__keylist_k_nscore__int_I11I) (valI96I Int)) Result@nscore__keylist_k_nscore__int_I11I
(let ((_tmp_4I95I (nscore__keylist_k_nscore__int_I11I@nscore__keylist_k_nscore__int__hkeyI12I klI127I)))
(let ((_tmp_1I69I (< _tmp_4I95I valI96I)))
(let ((_tmp_0I65I (not _tmp_1I69I)))
(ite _tmp_0I65I
(let ((_tmp_6I64I (nscore__keylist_k_nscore__int_I11I@cons valI96I (bsqterm_object MIRNominalTypeEnum_nscore__keylist_k_nscore__int_I11I (cons@bsq_object_from_nscore__keylist_k_nscore__int_I11I klI127I)))))
(let ((___ir_ret___2I75I _tmp_6I64I))
(let ((___ir_ret___3I94I ___ir_ret___2I75I))
(let (($return ___ir_ret___3I94I))
(result_success@nscore__keylist_k_nscore__int_I11I $return)
)
)
)
)
(let ((_tmp_11I129I (nscore__keylist_k_nscore__int_I11I@nscore__keylist_k_nscore__int__tailI13I klI127I)))
(let ((tlI130I _tmp_11I129I))
(let ((_tmp_12I131I (= tlI130I bsqterm_none)))
(ite _tmp_12I131I
(let ((_tmp_18I132I (nscore__keylist_k_nscore__int_I11I@nscore__keylist_k_nscore__int__hkeyI12I klI127I)))
(let ((_tmp_19I133I (nscore__keylist_k_nscore__int_I11I@cons valI96I bsqterm_none)))
(let ((_tmp_15I134I (nscore__keylist_k_nscore__int_I11I@cons _tmp_18I132I (bsqterm_object MIRNominalTypeEnum_nscore__keylist_k_nscore__int_I11I (cons@bsq_object_from_nscore__keylist_k_nscore__int_I11I _tmp_19I133I)))))
(let ((___ir_ret___1I74I _tmp_15I134I))
(let ((___ir_ret___3I94I ___ir_ret___1I74I))
(let (($return ___ir_ret___3I94I))
(result_success@nscore__keylist_k_nscore__int_I11I $return)
)
)
)
)
)
)
(let ((_tmp_25I135I (nscore__keylist_k_nscore__int_I11I@nscore__keylist_k_nscore__int__hkeyI12I klI127I)))
(let ((@tmpvar@44 (result_error@nscore__keylist_k_nscore__int_I11I (result_bmc "default"))))
(ite (is-result_error@nscore__keylist_k_nscore__int_I11I @tmpvar@44)
@tmpvar@44
(let ((_tmp_26I136I (result_success_value@nscore__keylist_k_nscore__int_I11I @tmpvar@44)))
(let ((_tmp_22I137I (nscore__keylist_k_nscore__int_I11I@cons _tmp_25I135I (bsqterm_object MIRNominalTypeEnum_nscore__keylist_k_nscore__int_I11I (cons@bsq_object_from_nscore__keylist_k_nscore__int_I11I _tmp_26I136I)))))
(let ((___ir_ret__I66I _tmp_22I137I))
(let ((___ir_ret___3I94I ___ir_ret__I66I))
(let (($return ___ir_ret___3I94I))
(result_success@nscore__keylist_k_nscore__int_I11I $return)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
))
(define-fun nscore__keylist__s_insert_k_nscore__int_I128I@gas2 ((klI127I nscore__keylist_k_nscore__int_I11I) (valI96I Int)) Result@nscore__keylist_k_nscore__int_I11I
(let ((_tmp_4I95I (nscore__keylist_k_nscore__int_I11I@nscore__keylist_k_nscore__int__hkeyI12I klI127I)))
(let ((_tmp_1I69I (< _tmp_4I95I valI96I)))
(let ((_tmp_0I65I (not _tmp_1I69I)))
(ite _tmp_0I65I
(let ((_tmp_6I64I (nscore__keylist_k_nscore__int_I11I@cons valI96I (bsqterm_object MIRNominalTypeEnum_nscore__keylist_k_nscore__int_I11I (cons@bsq_object_from_nscore__keylist_k_nscore__int_I11I klI127I)))))
(let ((___ir_ret___2I75I _tmp_6I64I))
(let ((___ir_ret___3I94I ___ir_ret___2I75I))
(let (($return ___ir_ret___3I94I))
(result_success@nscore__keylist_k_nscore__int_I11I $return)
)
)
)
)
(let ((_tmp_11I129I (nscore__keylist_k_nscore__int_I11I@nscore__keylist_k_nscore__int__tailI13I klI127I)))
(let ((tlI130I _tmp_11I129I))
(let ((_tmp_12I131I (= tlI130I bsqterm_none)))
(ite _tmp_12I131I
(let ((_tmp_18I132I (nscore__keylist_k_nscore__int_I11I@nscore__keylist_k_nscore__int__hkeyI12I klI127I)))
(let ((_tmp_19I133I (nscore__keylist_k_nscore__int_I11I@cons valI96I bsqterm_none)))
(let ((_tmp_15I134I (nscore__keylist_k_nscore__int_I11I@cons _tmp_18I132I (bsqterm_object MIRNominalTypeEnum_nscore__keylist_k_nscore__int_I11I (cons@bsq_object_from_nscore__keylist_k_nscore__int_I11I _tmp_19I133I)))))
(let ((___ir_ret___1I74I _tmp_15I134I))
(let ((___ir_ret___3I94I ___ir_ret___1I74I))
(let (($return ___ir_ret___3I94I))
(result_success@nscore__keylist_k_nscore__int_I11I $return)
)
)
)
)
)
)
(let ((_tmp_25I135I (nscore__keylist_k_nscore__int_I11I@nscore__keylist_k_nscore__int__hkeyI12I klI127I)))
(let ((@tmpvar@45 (nscore__keylist__s_insert_k_nscore__int_I128I@gas1 (bsqterm_object_nscore__keylist_k_nscore__int_I11I_value (bsqterm_object_value tlI130I)) valI96I)))
(ite (is-result_error@nscore__keylist_k_nscore__int_I11I @tmpvar@45)
@tmpvar@45
(let ((_tmp_26I136I (result_success_value@nscore__keylist_k_nscore__int_I11I @tmpvar@45)))
(let ((_tmp_22I137I (nscore__keylist_k_nscore__int_I11I@cons _tmp_25I135I (bsqterm_object MIRNominalTypeEnum_nscore__keylist_k_nscore__int_I11I (cons@bsq_object_from_nscore__keylist_k_nscore__int_I11I _tmp_26I136I)))))
(let ((___ir_ret__I66I _tmp_22I137I))
(let ((___ir_ret___3I94I ___ir_ret__I66I))
(let (($return ___ir_ret___3I94I))
(result_success@nscore__keylist_k_nscore__int_I11I $return)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
))
(define-fun nscore__keylist__s_insert_k_nscore__int_I128I@gas3 ((klI127I nscore__keylist_k_nscore__int_I11I) (valI96I Int)) Result@nscore__keylist_k_nscore__int_I11I
(let ((_tmp_4I95I (nscore__keylist_k_nscore__int_I11I@nscore__keylist_k_nscore__int__hkeyI12I klI127I)))
(let ((_tmp_1I69I (< _tmp_4I95I valI96I)))
(let ((_tmp_0I65I (not _tmp_1I69I)))
(ite _tmp_0I65I
(let ((_tmp_6I64I (nscore__keylist_k_nscore__int_I11I@cons valI96I (bsqterm_object MIRNominalTypeEnum_nscore__keylist_k_nscore__int_I11I (cons@bsq_object_from_nscore__keylist_k_nscore__int_I11I klI127I)))))
(let ((___ir_ret___2I75I _tmp_6I64I))
(let ((___ir_ret___3I94I ___ir_ret___2I75I))
(let (($return ___ir_ret___3I94I))
(result_success@nscore__keylist_k_nscore__int_I11I $return)
)
)
)
)
(let ((_tmp_11I129I (nscore__keylist_k_nscore__int_I11I@nscore__keylist_k_nscore__int__tailI13I klI127I)))
(let ((tlI130I _tmp_11I129I))
(let ((_tmp_12I131I (= tlI130I bsqterm_none)))
(ite _tmp_12I131I
(let ((_tmp_18I132I (nscore__keylist_k_nscore__int_I11I@nscore__keylist_k_nscore__int__hkeyI12I klI127I)))
(let ((_tmp_19I133I (nscore__keylist_k_nscore__int_I11I@cons valI96I bsqterm_none)))
(let ((_tmp_15I134I (nscore__keylist_k_nscore__int_I11I@cons _tmp_18I132I (bsqterm_object MIRNominalTypeEnum_nscore__keylist_k_nscore__int_I11I (cons@bsq_object_from_nscore__keylist_k_nscore__int_I11I _tmp_19I133I)))))
(let ((___ir_ret___1I74I _tmp_15I134I))
(let ((___ir_ret___3I94I ___ir_ret___1I74I))
(let (($return ___ir_ret___3I94I))
(result_success@nscore__keylist_k_nscore__int_I11I $return)
)
)
)
)
)
)
(let ((_tmp_25I135I (nscore__keylist_k_nscore__int_I11I@nscore__keylist_k_nscore__int__hkeyI12I klI127I)))
(let ((@tmpvar@46 (nscore__keylist__s_insert_k_nscore__int_I128I@gas2 (bsqterm_object_nscore__keylist_k_nscore__int_I11I_value (bsqterm_object_value tlI130I)) valI96I)))
(ite (is-result_error@nscore__keylist_k_nscore__int_I11I @tmpvar@46)
@tmpvar@46
(let ((_tmp_26I136I (result_success_value@nscore__keylist_k_nscore__int_I11I @tmpvar@46)))
(let ((_tmp_22I137I (nscore__keylist_k_nscore__int_I11I@cons _tmp_25I135I (bsqterm_object MIRNominalTypeEnum_nscore__keylist_k_nscore__int_I11I (cons@bsq_object_from_nscore__keylist_k_nscore__int_I11I _tmp_26I136I)))))
(let ((___ir_ret__I66I _tmp_22I137I))
(let ((___ir_ret___3I94I ___ir_ret__I66I))
(let (($return ___ir_ret___3I94I))
(result_success@nscore__keylist_k_nscore__int_I11I $return)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
))
(define-fun nscore__keylist__s_insert_k_nscore__int_I128I ((klI127I nscore__keylist_k_nscore__int_I11I) (valI96I Int)) Result@nscore__keylist_k_nscore__int_I11I
(let ((_tmp_4I95I (nscore__keylist_k_nscore__int_I11I@nscore__keylist_k_nscore__int__hkeyI12I klI127I)))
(let ((_tmp_1I69I (< _tmp_4I95I valI96I)))
(let ((_tmp_0I65I (not _tmp_1I69I)))
(ite _tmp_0I65I
(let ((_tmp_6I64I (nscore__keylist_k_nscore__int_I11I@cons valI96I (bsqterm_object MIRNominalTypeEnum_nscore__keylist_k_nscore__int_I11I (cons@bsq_object_from_nscore__keylist_k_nscore__int_I11I klI127I)))))
(let ((___ir_ret___2I75I _tmp_6I64I))
(let ((___ir_ret___3I94I ___ir_ret___2I75I))
(let (($return ___ir_ret___3I94I))
(result_success@nscore__keylist_k_nscore__int_I11I $return)
)
)
)
)
(let ((_tmp_11I129I (nscore__keylist_k_nscore__int_I11I@nscore__keylist_k_nscore__int__tailI13I klI127I)))
(let ((tlI130I _tmp_11I129I))
(let ((_tmp_12I131I (= tlI130I bsqterm_none)))
(ite _tmp_12I131I
(let ((_tmp_18I132I (nscore__keylist_k_nscore__int_I11I@nscore__keylist_k_nscore__int__hkeyI12I klI127I)))
(let ((_tmp_19I133I (nscore__keylist_k_nscore__int_I11I@cons valI96I bsqterm_none)))
(let ((_tmp_15I134I (nscore__keylist_k_nscore__int_I11I@cons _tmp_18I132I (bsqterm_object MIRNominalTypeEnum_nscore__keylist_k_nscore__int_I11I (cons@bsq_object_from_nscore__keylist_k_nscore__int_I11I _tmp_19I133I)))))
(let ((___ir_ret___1I74I _tmp_15I134I))
(let ((___ir_ret___3I94I ___ir_ret___1I74I))
(let (($return ___ir_ret___3I94I))
(result_success@nscore__keylist_k_nscore__int_I11I $return)
)
)
)
)
)
)
(let ((_tmp_25I135I (nscore__keylist_k_nscore__int_I11I@nscore__keylist_k_nscore__int__hkeyI12I klI127I)))
(let ((@tmpvar@47 (nscore__keylist__s_insert_k_nscore__int_I128I@gas3 (bsqterm_object_nscore__keylist_k_nscore__int_I11I_value (bsqterm_object_value tlI130I)) valI96I)))
(ite (is-result_error@nscore__keylist_k_nscore__int_I11I @tmpvar@47)
@tmpvar@47
(let ((_tmp_26I136I (result_success_value@nscore__keylist_k_nscore__int_I11I @tmpvar@47)))
(let ((_tmp_22I137I (nscore__keylist_k_nscore__int_I11I@cons _tmp_25I135I (bsqterm_object MIRNominalTypeEnum_nscore__keylist_k_nscore__int_I11I (cons@bsq_object_from_nscore__keylist_k_nscore__int_I11I _tmp_26I136I)))))
(let ((___ir_ret__I66I _tmp_22I137I))
(let ((___ir_ret___3I94I ___ir_ret__I66I))
(let (($return ___ir_ret___3I94I))
(result_success@nscore__keylist_k_nscore__int_I11I $return)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
))
(define-fun nscore__keylist__s_sort_k_nscore__int_I139I@gas1 ((klI127I nscore__keylist_k_nscore__int_I11I) (rklI138I nscore__keylist_k_nscore__int_I11I)) Result@nscore__keylist_k_nscore__int_I11I
(let ((_tmp_2I104I (nscore__keylist_k_nscore__int_I11I@nscore__keylist_k_nscore__int__tailI13I klI127I)))
(let ((tlI130I _tmp_2I104I))
(let ((_tmp_3I62I (= tlI130I bsqterm_none)))
(ite _tmp_3I62I
(let ((_tmp_10I100I (nscore__keylist_k_nscore__int_I11I@nscore__keylist_k_nscore__int__hkeyI12I klI127I)))
(let ((@tmpvar@48 (nscore__keylist__s_insert_k_nscore__int_I128I rklI138I _tmp_10I100I)))
(ite (is-result_error@nscore__keylist_k_nscore__int_I11I @tmpvar@48)
@tmpvar@48
(let ((_tmp_6I64I (result_success_value@nscore__keylist_k_nscore__int_I11I @tmpvar@48)))
(let ((___ir_ret___1I74I _tmp_6I64I))
(let ((___ir_ret___2I75I ___ir_ret___1I74I))
(let (($return ___ir_ret___2I75I))
(result_success@nscore__keylist_k_nscore__int_I11I $return)
)
)
)
)
)
)
)
(let ((_tmp_17I140I (nscore__keylist_k_nscore__int_I11I@nscore__keylist_k_nscore__int__hkeyI12I klI127I)))
(let ((@tmpvar@49 (nscore__keylist__s_insert_k_nscore__int_I128I rklI138I _tmp_17I140I)))
(ite (is-result_error@nscore__keylist_k_nscore__int_I11I @tmpvar@49)
@tmpvar@49
(let ((_tmp_13I98I (result_success_value@nscore__keylist_k_nscore__int_I11I @tmpvar@49)))
(let ((@tmpvar@50 (result_error@nscore__keylist_k_nscore__int_I11I (result_bmc "default"))))
(ite (is-result_error@nscore__keylist_k_nscore__int_I11I @tmpvar@50)
@tmpvar@50
(let ((_tmp_11I129I (result_success_value@nscore__keylist_k_nscore__int_I11I @tmpvar@50)))
(let ((___ir_ret__I66I _tmp_11I129I))
(let ((___ir_ret___2I75I ___ir_ret__I66I))
(let (($return ___ir_ret___2I75I))
(result_success@nscore__keylist_k_nscore__int_I11I $return)
)
)
)
)
)
)
)
)
)
)
)
)
)
))
(define-fun nscore__keylist__s_sort_k_nscore__int_I139I@gas2 ((klI127I nscore__keylist_k_nscore__int_I11I) (rklI138I nscore__keylist_k_nscore__int_I11I)) Result@nscore__keylist_k_nscore__int_I11I
(let ((_tmp_2I104I (nscore__keylist_k_nscore__int_I11I@nscore__keylist_k_nscore__int__tailI13I klI127I)))
(let ((tlI130I _tmp_2I104I))
(let ((_tmp_3I62I (= tlI130I bsqterm_none)))
(ite _tmp_3I62I
(let ((_tmp_10I100I (nscore__keylist_k_nscore__int_I11I@nscore__keylist_k_nscore__int__hkeyI12I klI127I)))
(let ((@tmpvar@51 (nscore__keylist__s_insert_k_nscore__int_I128I rklI138I _tmp_10I100I)))
(ite (is-result_error@nscore__keylist_k_nscore__int_I11I @tmpvar@51)
@tmpvar@51
(let ((_tmp_6I64I (result_success_value@nscore__keylist_k_nscore__int_I11I @tmpvar@51)))
(let ((___ir_ret___1I74I _tmp_6I64I))
(let ((___ir_ret___2I75I ___ir_ret___1I74I))
(let (($return ___ir_ret___2I75I))
(result_success@nscore__keylist_k_nscore__int_I11I $return)
)
)
)
)
)
)
)
(let ((_tmp_17I140I (nscore__keylist_k_nscore__int_I11I@nscore__keylist_k_nscore__int__hkeyI12I klI127I)))
(let ((@tmpvar@52 (nscore__keylist__s_insert_k_nscore__int_I128I rklI138I _tmp_17I140I)))
(ite (is-result_error@nscore__keylist_k_nscore__int_I11I @tmpvar@52)
@tmpvar@52
(let ((_tmp_13I98I (result_success_value@nscore__keylist_k_nscore__int_I11I @tmpvar@52)))
(let ((@tmpvar@53 (nscore__keylist__s_sort_k_nscore__int_I139I@gas1 (bsqterm_object_nscore__keylist_k_nscore__int_I11I_value (bsqterm_object_value tlI130I)) _tmp_13I98I)))
(ite (is-result_error@nscore__keylist_k_nscore__int_I11I @tmpvar@53)
@tmpvar@53
(let ((_tmp_11I129I (result_success_value@nscore__keylist_k_nscore__int_I11I @tmpvar@53)))
(let ((___ir_ret__I66I _tmp_11I129I))
(let ((___ir_ret___2I75I ___ir_ret__I66I))
(let (($return ___ir_ret___2I75I))
(result_success@nscore__keylist_k_nscore__int_I11I $return)
)
)
)
)
)
)
)
)
)
)
)
)
)
))
(define-fun nscore__keylist__s_sort_k_nscore__int_I139I@gas3 ((klI127I nscore__keylist_k_nscore__int_I11I) (rklI138I nscore__keylist_k_nscore__int_I11I)) Result@nscore__keylist_k_nscore__int_I11I
(let ((_tmp_2I104I (nscore__keylist_k_nscore__int_I11I@nscore__keylist_k_nscore__int__tailI13I klI127I)))
(let ((tlI130I _tmp_2I104I))
(let ((_tmp_3I62I (= tlI130I bsqterm_none)))
(ite _tmp_3I62I
(let ((_tmp_10I100I (nscore__keylist_k_nscore__int_I11I@nscore__keylist_k_nscore__int__hkeyI12I klI127I)))
(let ((@tmpvar@54 (nscore__keylist__s_insert_k_nscore__int_I128I rklI138I _tmp_10I100I)))
(ite (is-result_error@nscore__keylist_k_nscore__int_I11I @tmpvar@54)
@tmpvar@54
(let ((_tmp_6I64I (result_success_value@nscore__keylist_k_nscore__int_I11I @tmpvar@54)))
(let ((___ir_ret___1I74I _tmp_6I64I))
(let ((___ir_ret___2I75I ___ir_ret___1I74I))
(let (($return ___ir_ret___2I75I))
(result_success@nscore__keylist_k_nscore__int_I11I $return)
)
)
)
)
)
)
)
(let ((_tmp_17I140I (nscore__keylist_k_nscore__int_I11I@nscore__keylist_k_nscore__int__hkeyI12I klI127I)))
(let ((@tmpvar@55 (nscore__keylist__s_insert_k_nscore__int_I128I rklI138I _tmp_17I140I)))
(ite (is-result_error@nscore__keylist_k_nscore__int_I11I @tmpvar@55)
@tmpvar@55
(let ((_tmp_13I98I (result_success_value@nscore__keylist_k_nscore__int_I11I @tmpvar@55)))
(let ((@tmpvar@56 (nscore__keylist__s_sort_k_nscore__int_I139I@gas2 (bsqterm_object_nscore__keylist_k_nscore__int_I11I_value (bsqterm_object_value tlI130I)) _tmp_13I98I)))
(ite (is-result_error@nscore__keylist_k_nscore__int_I11I @tmpvar@56)
@tmpvar@56
(let ((_tmp_11I129I (result_success_value@nscore__keylist_k_nscore__int_I11I @tmpvar@56)))
(let ((___ir_ret__I66I _tmp_11I129I))
(let ((___ir_ret___2I75I ___ir_ret__I66I))
(let (($return ___ir_ret___2I75I))
(result_success@nscore__keylist_k_nscore__int_I11I $return)
)
)
)
)
)
)
)
)
)
)
)
)
)
))
(define-fun nscore__keylist__s_sort_k_nscore__int_I139I ((klI127I nscore__keylist_k_nscore__int_I11I) (rklI138I nscore__keylist_k_nscore__int_I11I)) Result@nscore__keylist_k_nscore__int_I11I
(let ((_tmp_2I104I (nscore__keylist_k_nscore__int_I11I@nscore__keylist_k_nscore__int__tailI13I klI127I)))
(let ((tlI130I _tmp_2I104I))
(let ((_tmp_3I62I (= tlI130I bsqterm_none)))
(ite _tmp_3I62I
(let ((_tmp_10I100I (nscore__keylist_k_nscore__int_I11I@nscore__keylist_k_nscore__int__hkeyI12I klI127I)))
(let ((@tmpvar@57 (nscore__keylist__s_insert_k_nscore__int_I128I rklI138I _tmp_10I100I)))
(ite (is-result_error@nscore__keylist_k_nscore__int_I11I @tmpvar@57)
@tmpvar@57
(let ((_tmp_6I64I (result_success_value@nscore__keylist_k_nscore__int_I11I @tmpvar@57)))
(let ((___ir_ret___1I74I _tmp_6I64I))
(let ((___ir_ret___2I75I ___ir_ret___1I74I))
(let (($return ___ir_ret___2I75I))
(result_success@nscore__keylist_k_nscore__int_I11I $return)
)
)
)
)
)
)
)
(let ((_tmp_17I140I (nscore__keylist_k_nscore__int_I11I@nscore__keylist_k_nscore__int__hkeyI12I klI127I)))
(let ((@tmpvar@58 (nscore__keylist__s_insert_k_nscore__int_I128I rklI138I _tmp_17I140I)))
(ite (is-result_error@nscore__keylist_k_nscore__int_I11I @tmpvar@58)
@tmpvar@58
(let ((_tmp_13I98I (result_success_value@nscore__keylist_k_nscore__int_I11I @tmpvar@58)))
(let ((@tmpvar@59 (nscore__keylist__s_sort_k_nscore__int_I139I@gas3 (bsqterm_object_nscore__keylist_k_nscore__int_I11I_value (bsqterm_object_value tlI130I)) _tmp_13I98I)))
(ite (is-result_error@nscore__keylist_k_nscore__int_I11I @tmpvar@59)
@tmpvar@59
(let ((_tmp_11I129I (result_success_value@nscore__keylist_k_nscore__int_I11I @tmpvar@59)))
(let ((___ir_ret__I66I _tmp_11I129I))
(let ((___ir_ret___2I75I ___ir_ret__I66I))
(let (($return ___ir_ret___2I75I))
(result_success@nscore__keylist_k_nscore__int_I11I $return)
)
)
)
)
)
)
)
)
)
)
)
)
)
))
(define-fun nscore__keylist__sort_k_nscore__int_I141I ((klI127I BTerm)) Result@BTerm
(let ((_tmp_0I65I (= klI127I bsqterm_none)))
(ite _tmp_0I65I
(let ((___ir_ret___2I75I bsqkey_none))
(let ((___ir_ret___3I94I bsqterm_none))
(let (($return ___ir_ret___3I94I))
(result_success@BTerm $return)
)
)
)
(let ((_tmp_6I64I (nscore__keylist_k_nscore__int_I11I@nscore__keylist_k_nscore__int__tailI13I (bsqterm_object_nscore__keylist_k_nscore__int_I11I_value (bsqterm_object_value klI127I)))))
(let ((tlI130I _tmp_6I64I))
(let ((_tmp_7I97I (= tlI130I bsqterm_none)))
(ite _tmp_7I97I
(let ((___ir_ret___1I74I klI127I))
(let ((___ir_ret___3I94I ___ir_ret___1I74I))
(let (($return ___ir_ret___3I94I))
(result_success@BTerm $return)
)
)
)
(let ((_tmp_16I99I (nscore__keylist_k_nscore__int_I11I@nscore__keylist_k_nscore__int__hkeyI12I (bsqterm_object_nscore__keylist_k_nscore__int_I11I_value (bsqterm_object_value klI127I)))))
(let ((_tmp_13I98I (nscore__keylist_k_nscore__int_I11I@cons _tmp_16I99I bsqterm_none)))
(let ((@tmpvar@60 (nscore__keylist__s_sort_k_nscore__int_I139I (bsqterm_object_nscore__keylist_k_nscore__int_I11I_value (bsqterm_object_value tlI130I)) _tmp_13I98I)))
(ite (is-result_error@nscore__keylist_k_nscore__int_I11I @tmpvar@60)
(result_error@BTerm (result_error_code@nscore__keylist_k_nscore__int_I11I @tmpvar@60))
(let ((_tmp_11I129I (result_success_value@nscore__keylist_k_nscore__int_I11I @tmpvar@60)))
(let ((___ir_ret__I66I _tmp_11I129I))
(let ((___ir_ret___3I94I (bsqterm_object MIRNominalTypeEnum_nscore__keylist_k_nscore__int_I11I (cons@bsq_object_from_nscore__keylist_k_nscore__int_I11I ___ir_ret__I66I))))
(let (($return ___ir_ret___3I94I))
(result_success@BTerm $return)
)
)
)
)
)
)
)
)
)
)
)
)
)
))
(define-fun nscore__list__s_unsafe_push_t_nscore__int_I142I ((lI81I nscore__list_t_nscore__int_I17I) (vI88I Int)) nscore__list_t_nscore__int_I17I
(nscore__list_t_nscore__int_I17I@cons (+ (nscore__list_t_nscore__int_I17I@@size lI81I) 1) (store (nscore__list_t_nscore__int_I17I@@entries lI81I) (nscore__list_t_nscore__int_I17I@@size lI81I) vI88I))
)
(define-fun nscore__map__s_key_list_k_nscore__int__v_nscore__list_nsmain__func__I143I@gas1 ((klI127I BTerm) (lI81I nscore__list_t_nscore__int_I17I)) Result@nscore__list_t_nscore__int_I17I
(let ((_tmp_0I65I (= klI127I bsqterm_none)))
(ite _tmp_0I65I
(let ((___ir_ret___1I74I lI81I))
(let ((___ir_ret___2I75I ___ir_ret___1I74I))
(let (($return ___ir_ret___2I75I))
(result_success@nscore__list_t_nscore__int_I17I $return)
)
)
)
(let ((_tmp_7I97I (nscore__keylist_k_nscore__int_I11I@nscore__keylist_k_nscore__int__tailI13I (bsqterm_object_nscore__keylist_k_nscore__int_I11I_value (bsqterm_object_value klI127I)))))
(let ((_tmp_12I131I (nscore__keylist_k_nscore__int_I11I@nscore__keylist_k_nscore__int__hkeyI12I (bsqterm_object_nscore__keylist_k_nscore__int_I11I_value (bsqterm_object_value klI127I)))))
(let ((_tmp_8I144I (nscore__list__s_unsafe_push_t_nscore__int_I142I lI81I _tmp_12I131I)))
(let ((@tmpvar@61 (result_error@nscore__list_t_nscore__int_I17I (result_bmc "collection"))))
(ite (is-result_error@nscore__list_t_nscore__int_I17I @tmpvar@61)
@tmpvar@61
(let ((_tmp_4I95I (result_success_value@nscore__list_t_nscore__int_I17I @tmpvar@61)))
(let ((___ir_ret__I66I _tmp_4I95I))
(let ((___ir_ret___2I75I ___ir_ret__I66I))
(let (($return ___ir_ret___2I75I))
(result_success@nscore__list_t_nscore__int_I17I $return)
)
)
)
)
)
)
)
)
)
)
))
(define-fun nscore__map__s_key_list_k_nscore__int__v_nscore__list_nsmain__func__I143I@gas2 ((klI127I BTerm) (lI81I nscore__list_t_nscore__int_I17I)) Result@nscore__list_t_nscore__int_I17I
(let ((_tmp_0I65I (= klI127I bsqterm_none)))
(ite _tmp_0I65I
(let ((___ir_ret___1I74I lI81I))
(let ((___ir_ret___2I75I ___ir_ret___1I74I))
(let (($return ___ir_ret___2I75I))
(result_success@nscore__list_t_nscore__int_I17I $return)
)
)
)
(let ((_tmp_7I97I (nscore__keylist_k_nscore__int_I11I@nscore__keylist_k_nscore__int__tailI13I (bsqterm_object_nscore__keylist_k_nscore__int_I11I_value (bsqterm_object_value klI127I)))))
(let ((_tmp_12I131I (nscore__keylist_k_nscore__int_I11I@nscore__keylist_k_nscore__int__hkeyI12I (bsqterm_object_nscore__keylist_k_nscore__int_I11I_value (bsqterm_object_value klI127I)))))
(let ((_tmp_8I144I (nscore__list__s_unsafe_push_t_nscore__int_I142I lI81I _tmp_12I131I)))
(let ((@tmpvar@62 (nscore__map__s_key_list_k_nscore__int__v_nscore__list_nsmain__func__I143I@gas1 _tmp_7I97I _tmp_8I144I)))
(ite (is-result_error@nscore__list_t_nscore__int_I17I @tmpvar@62)
@tmpvar@62
(let ((_tmp_4I95I (result_success_value@nscore__list_t_nscore__int_I17I @tmpvar@62)))
(let ((___ir_ret__I66I _tmp_4I95I))
(let ((___ir_ret___2I75I ___ir_ret__I66I))
(let (($return ___ir_ret___2I75I))
(result_success@nscore__list_t_nscore__int_I17I $return)
)
)
)
)
)
)
)
)
)
)
))
(define-fun nscore__map__s_key_list_k_nscore__int__v_nscore__list_nsmain__func__I143I@gas3 ((klI127I BTerm) (lI81I nscore__list_t_nscore__int_I17I)) Result@nscore__list_t_nscore__int_I17I
(let ((_tmp_0I65I (= klI127I bsqterm_none)))
(ite _tmp_0I65I
(let ((___ir_ret___1I74I lI81I))
(let ((___ir_ret___2I75I ___ir_ret___1I74I))
(let (($return ___ir_ret___2I75I))
(result_success@nscore__list_t_nscore__int_I17I $return)
)
)
)
(let ((_tmp_7I97I (nscore__keylist_k_nscore__int_I11I@nscore__keylist_k_nscore__int__tailI13I (bsqterm_object_nscore__keylist_k_nscore__int_I11I_value (bsqterm_object_value klI127I)))))
(let ((_tmp_12I131I (nscore__keylist_k_nscore__int_I11I@nscore__keylist_k_nscore__int__hkeyI12I (bsqterm_object_nscore__keylist_k_nscore__int_I11I_value (bsqterm_object_value klI127I)))))
(let ((_tmp_8I144I (nscore__list__s_unsafe_push_t_nscore__int_I142I lI81I _tmp_12I131I)))
(let ((@tmpvar@63 (nscore__map__s_key_list_k_nscore__int__v_nscore__list_nsmain__func__I143I@gas2 _tmp_7I97I _tmp_8I144I)))
(ite (is-result_error@nscore__list_t_nscore__int_I17I @tmpvar@63)
@tmpvar@63
(let ((_tmp_4I95I (result_success_value@nscore__list_t_nscore__int_I17I @tmpvar@63)))
(let ((___ir_ret__I66I _tmp_4I95I))
(let ((___ir_ret___2I75I ___ir_ret__I66I))
(let (($return ___ir_ret___2I75I))
(result_success@nscore__list_t_nscore__int_I17I $return)
)
)
)
)
)
)
)
)
)
)
))
(define-fun nscore__map__s_key_list_k_nscore__int__v_nscore__list_nsmain__func__I143I@gas4 ((klI127I BTerm) (lI81I nscore__list_t_nscore__int_I17I)) Result@nscore__list_t_nscore__int_I17I
(let ((_tmp_0I65I (= klI127I bsqterm_none)))
(ite _tmp_0I65I
(let ((___ir_ret___1I74I lI81I))
(let ((___ir_ret___2I75I ___ir_ret___1I74I))
(let (($return ___ir_ret___2I75I))
(result_success@nscore__list_t_nscore__int_I17I $return)
)
)
)
(let ((_tmp_7I97I (nscore__keylist_k_nscore__int_I11I@nscore__keylist_k_nscore__int__tailI13I (bsqterm_object_nscore__keylist_k_nscore__int_I11I_value (bsqterm_object_value klI127I)))))
(let ((_tmp_12I131I (nscore__keylist_k_nscore__int_I11I@nscore__keylist_k_nscore__int__hkeyI12I (bsqterm_object_nscore__keylist_k_nscore__int_I11I_value (bsqterm_object_value klI127I)))))
(let ((_tmp_8I144I (nscore__list__s_unsafe_push_t_nscore__int_I142I lI81I _tmp_12I131I)))
(let ((@tmpvar@64 (nscore__map__s_key_list_k_nscore__int__v_nscore__list_nsmain__func__I143I@gas3 _tmp_7I97I _tmp_8I144I)))
(ite (is-result_error@nscore__list_t_nscore__int_I17I @tmpvar@64)
@tmpvar@64
(let ((_tmp_4I95I (result_success_value@nscore__list_t_nscore__int_I17I @tmpvar@64)))
(let ((___ir_ret__I66I _tmp_4I95I))
(let ((___ir_ret___2I75I ___ir_ret__I66I))
(let (($return ___ir_ret___2I75I))
(result_success@nscore__list_t_nscore__int_I17I $return)
)
)
)
)
)
)
)
)
)
)
))
(define-fun nscore__map__s_key_list_k_nscore__int__v_nscore__list_nsmain__func__I143I ((klI127I BTerm) (lI81I nscore__list_t_nscore__int_I17I)) Result@nscore__list_t_nscore__int_I17I
(let ((_tmp_0I65I (= klI127I bsqterm_none)))
(ite _tmp_0I65I
(let ((___ir_ret___1I74I lI81I))
(let ((___ir_ret___2I75I ___ir_ret___1I74I))
(let (($return ___ir_ret___2I75I))
(result_success@nscore__list_t_nscore__int_I17I $return)
)
)
)
(let ((_tmp_7I97I (nscore__keylist_k_nscore__int_I11I@nscore__keylist_k_nscore__int__tailI13I (bsqterm_object_nscore__keylist_k_nscore__int_I11I_value (bsqterm_object_value klI127I)))))
(let ((_tmp_12I131I (nscore__keylist_k_nscore__int_I11I@nscore__keylist_k_nscore__int__hkeyI12I (bsqterm_object_nscore__keylist_k_nscore__int_I11I_value (bsqterm_object_value klI127I)))))
(let ((_tmp_8I144I (nscore__list__s_unsafe_push_t_nscore__int_I142I lI81I _tmp_12I131I)))
(let ((@tmpvar@65 (nscore__map__s_key_list_k_nscore__int__v_nscore__list_nsmain__func__I143I@gas4 _tmp_7I97I _tmp_8I144I)))
(ite (is-result_error@nscore__list_t_nscore__int_I17I @tmpvar@65)
@tmpvar@65
(let ((_tmp_4I95I (result_success_value@nscore__list_t_nscore__int_I17I @tmpvar@65)))
(let ((___ir_ret__I66I _tmp_4I95I))
(let ((___ir_ret___2I75I ___ir_ret__I66I))
(let (($return ___ir_ret___2I75I))
(result_success@nscore__list_t_nscore__int_I17I $return)
)
)
)
)
)
)
)
)
)
)
))
(define-fun nscore__map__keys_k_nscore__int__v_nscore__list_nsmain__func__I145I ((thisI79I nscore__map_k_nscore__int__v_nscore__list_nsmain__func__I23I)) Result@nscore__list_t_nscore__int_I17I
(let ((_tmp_2I104I (nscore__map__s_get_keylist_k_nscore__int__v_nscore__list_nsmain__func__I126I thisI79I)))
(let ((@tmpvar@66 (nscore__keylist__sort_k_nscore__int_I141I _tmp_2I104I)))
(ite (is-result_error@BTerm @tmpvar@66)
(result_error@nscore__list_t_nscore__int_I17I (result_error_code@BTerm @tmpvar@66))
(let ((_tmp_1I69I (result_success_value@BTerm @tmpvar@66)))
(let ((_tmp_4I95I (nscore__list_t_nscore__int_I17I@cons 0 nscore__list_t_nscore__int__collection_data_array_emptyI18I)))
(let ((@tmpvar@67 (nscore__map__s_key_list_k_nscore__int__v_nscore__list_nsmain__func__I143I _tmp_1I69I _tmp_4I95I)))
(ite (is-result_error@nscore__list_t_nscore__int_I17I @tmpvar@67)
@tmpvar@67
(let ((_tmp_0I65I (result_success_value@nscore__list_t_nscore__int_I17I @tmpvar@67)))
(let ((___ir_ret__I66I _tmp_0I65I))
(let (($return ___ir_ret__I66I))
(result_success@nscore__list_t_nscore__int_I17I $return)
)
)
)
)
)
)
)
)
)
))
(define-fun nscore__list__get_t_nscore__int___pre__llogic_done_3I147I ((_tmp_0_2I146I Bool)) Result@Bool
(let ((___ir_ret__I66I _tmp_0_2I146I))
(let (($return ___ir_ret__I66I))
(result_success@Bool $return)
)
))
(define-fun nscore__list__s_size_t_nscore__int_I148I ((lI81I nscore__list_t_nscore__int_I17I)) Int
(nscore__list_t_nscore__int_I17I@@size lI81I)
)
(define-fun nscore__list__get_t_nscore__int___preI149I ((thisI79I nscore__list_t_nscore__int_I17I) (iI83I Int)) Result@Bool
(let ((_tmp_1I69I (or (< 0 iI83I) (= 0 iI83I))))
(ite _tmp_1I69I
(let ((_tmp_6I64I (nscore__list__s_size_t_nscore__int_I148I thisI79I)))
(let ((_tmp_4I95I (< iI83I _tmp_6I64I)))
(let ((_tmp_0_1I73I _tmp_4I95I))
(let ((@tmpvar@68 (nscore__list__get_t_nscore__int___pre__llogic_done_3I147I _tmp_0_1I73I)))
(ite (is-result_error@Bool @tmpvar@68)
@tmpvar@68
(let ((_tmp_100001I150I (result_success_value@Bool @tmpvar@68)))
(let (($return _tmp_100001I150I))
(result_success@Bool $return)
)
)
)
)
)
)
)
(let ((_tmp_0I65I false))
(let ((@tmpvar@69 (nscore__list__get_t_nscore__int___pre__llogic_done_3I147I _tmp_0I65I)))
(ite (is-result_error@Bool @tmpvar@69)
@tmpvar@69
(let ((_tmp_100000I151I (result_success_value@Bool @tmpvar@69)))
(let (($return _tmp_100000I151I))
(result_success@Bool $return)
)
)
)
)
)
)
))
(define-fun nscore__list__s_unsafe_get_t_nscore__int_I152I ((lI81I nscore__list_t_nscore__int_I17I) (iI83I Int)) Int
(select (nscore__list_t_nscore__int_I17I@@entries lI81I) iI83I)
)
(define-fun nscore__list__get_t_nscore__int_I153I ((thisI79I nscore__list_t_nscore__int_I17I) (iI83I Int)) Result@Int
(let ((@tmpvar@70 (nscore__list__get_t_nscore__int___preI149I thisI79I iI83I)))
(ite (is-result_error@Bool @tmpvar@70)
(result_error@Int (result_error_code@Bool @tmpvar@70))
(let ((_tmp_0I65I (result_success_value@Bool @tmpvar@70)))
(ite _tmp_0I65I
(let ((_tmp_1I69I (nscore__list__s_unsafe_get_t_nscore__int_I152I thisI79I iI83I)))
(let ((___ir_ret__I66I _tmp_1I69I))
(let (($return ___ir_ret__I66I))
(result_success@Int $return)
)
)
)
(result_error@Int (result_error 3))
)
)
)
))
(define-fun nscore__map__get_k_nscore__int__v_nscore__list_nsmain__func____preI154I ((thisI79I nscore__map_k_nscore__int__v_nscore__list_nsmain__func__I23I) (keyI77I Int)) Result@Bool
(let ((_tmp_0I65I (nscore__map__s_has_key_k_nscore__int__v_nscore__list_nsmain__func__I78I thisI79I keyI77I)))
(let ((___ir_ret__I66I _tmp_0I65I))
(let (($return ___ir_ret__I66I))
(result_success@Bool $return)
)
)
))
(define-fun nscore__map__s_at_val_k_nscore__int__v_nscore__list_nsmain__func__I155I ((mI76I nscore__map_k_nscore__int__v_nscore__list_nsmain__func__I23I) (keyI77I Int)) nscore__list_t_nsmain__func_I19I
(select (nscore__map_k_nscore__int__v_nscore__list_nsmain__func__I23I@@values mI76I) keyI77I)
)
(define-fun nscore__map__get_k_nscore__int__v_nscore__list_nsmain__func__I156I ((thisI79I nscore__map_k_nscore__int__v_nscore__list_nsmain__func__I23I) (keyI77I Int)) Result@nscore__list_t_nsmain__func_I19I
(let ((@tmpvar@71 (nscore__map__get_k_nscore__int__v_nscore__list_nsmain__func____preI154I thisI79I keyI77I)))
(ite (is-result_error@Bool @tmpvar@71)
(result_error@nscore__list_t_nsmain__func_I19I (result_error_code@Bool @tmpvar@71))
(let ((_tmp_0I65I (result_success_value@Bool @tmpvar@71)))
(ite _tmp_0I65I
(let ((_tmp_1I69I (nscore__map__s_at_val_k_nscore__int__v_nscore__list_nsmain__func__I155I thisI79I keyI77I)))
(let ((___ir_ret__I66I _tmp_1I69I))
(let (($return ___ir_ret__I66I))
(result_success@nscore__list_t_nsmain__func_I19I $return)
)
)
)
(result_error@nscore__list_t_nsmain__func_I19I (result_error 4))
)
)
)
))
(define-fun nscore__list__s_size_t_nsmain__func_I157I ((lI81I nscore__list_t_nsmain__func_I19I)) Int
(nscore__list_t_nsmain__func_I19I@@size lI81I)
)
(define-fun nscore__list__s_unsafe_get_t_nsmain__func_I158I ((lI81I nscore__list_t_nsmain__func_I19I) (iI83I Int)) nsmain__funcI20I
(select (nscore__list_t_nsmain__func_I19I@@entries lI81I) iI83I)
)
(define-fun nscore__list__s_unsafe_push_t_nsmain__func_I159I ((lI81I nscore__list_t_nsmain__func_I19I) (vI88I nsmain__funcI20I)) nscore__list_t_nsmain__func_I19I
(nscore__list_t_nsmain__func_I19I@cons (+ (nscore__list_t_nsmain__func_I19I@@size lI81I) 1) (store (nscore__list_t_nsmain__func_I19I@@entries lI81I) (nscore__list_t_nsmain__func_I19I@@size lI81I) vI88I))
)
(define-fun nscore__list__s_append_t_nsmain__func_I160I@gas1 ((lI81I nscore__list_t_nsmain__func_I19I) (lsizeI90I Int) (lpI91I nscore__list_t_nsmain__func_I19I) (idxI92I Int)) Result@nscore__list_t_nsmain__func_I19I
(let ((_tmp_0I65I (= idxI92I lsizeI90I)))
(ite _tmp_0I65I
(let ((___ir_ret___1I74I lpI91I))
(let ((___ir_ret___2I75I ___ir_ret___1I74I))
(let (($return ___ir_ret___2I75I))
(result_success@nscore__list_t_nsmain__func_I19I $return)
)
)
)
(let ((_tmp_4I95I (nscore__list__s_unsafe_get_t_nsmain__func_I158I lI81I idxI92I)))
(let ((valI96I _tmp_4I95I))
(let ((_tmp_10I100I (nscore__list__s_unsafe_push_t_nsmain__func_I159I lpI91I valI96I)))
(let ((_tmp_13I98I (+ idxI92I 1)))
(ite (@int_unsafe _tmp_13I98I)
(result_error@nscore__list_t_nsmain__func_I19I (result_error 2))
(let ((@tmpvar@72 (result_error@nscore__list_t_nsmain__func_I19I (result_bmc "collection"))))
(ite (is-result_error@nscore__list_t_nsmain__func_I19I @tmpvar@72)
@tmpvar@72
(let ((_tmp_7I97I (result_success_value@nscore__list_t_nsmain__func_I19I @tmpvar@72)))
(let ((___ir_ret__I66I _tmp_7I97I))
(let ((___ir_ret___2I75I ___ir_ret__I66I))
(let (($return ___ir_ret___2I75I))
(result_success@nscore__list_t_nsmain__func_I19I $return)
)
)
)
)
)
)
)
)
)
)
)
)
))
(define-fun nscore__list__s_append_t_nsmain__func_I160I@gas2 ((lI81I nscore__list_t_nsmain__func_I19I) (lsizeI90I Int) (lpI91I nscore__list_t_nsmain__func_I19I) (idxI92I Int)) Result@nscore__list_t_nsmain__func_I19I
(let ((_tmp_0I65I (= idxI92I lsizeI90I)))
(ite _tmp_0I65I
(let ((___ir_ret___1I74I lpI91I))
(let ((___ir_ret___2I75I ___ir_ret___1I74I))
(let (($return ___ir_ret___2I75I))
(result_success@nscore__list_t_nsmain__func_I19I $return)
)
)
)
(let ((_tmp_4I95I (nscore__list__s_unsafe_get_t_nsmain__func_I158I lI81I idxI92I)))
(let ((valI96I _tmp_4I95I))
(let ((_tmp_10I100I (nscore__list__s_unsafe_push_t_nsmain__func_I159I lpI91I valI96I)))
(let ((_tmp_13I98I (+ idxI92I 1)))
(ite (@int_unsafe _tmp_13I98I)
(result_error@nscore__list_t_nsmain__func_I19I (result_error 2))
(let ((@tmpvar@73 (nscore__list__s_append_t_nsmain__func_I160I@gas1 lI81I lsizeI90I _tmp_10I100I _tmp_13I98I)))
(ite (is-result_error@nscore__list_t_nsmain__func_I19I @tmpvar@73)
@tmpvar@73
(let ((_tmp_7I97I (result_success_value@nscore__list_t_nsmain__func_I19I @tmpvar@73)))
(let ((___ir_ret__I66I _tmp_7I97I))
(let ((___ir_ret___2I75I ___ir_ret__I66I))
(let (($return ___ir_ret___2I75I))
(result_success@nscore__list_t_nsmain__func_I19I $return)
)
)
)
)
)
)
)
)
)
)
)
)
))
(define-fun nscore__list__s_append_t_nsmain__func_I160I@gas3 ((lI81I nscore__list_t_nsmain__func_I19I) (lsizeI90I Int) (lpI91I nscore__list_t_nsmain__func_I19I) (idxI92I Int)) Result@nscore__list_t_nsmain__func_I19I
(let ((_tmp_0I65I (= idxI92I lsizeI90I)))
(ite _tmp_0I65I
(let ((___ir_ret___1I74I lpI91I))
(let ((___ir_ret___2I75I ___ir_ret___1I74I))
(let (($return ___ir_ret___2I75I))
(result_success@nscore__list_t_nsmain__func_I19I $return)
)
)
)
(let ((_tmp_4I95I (nscore__list__s_unsafe_get_t_nsmain__func_I158I lI81I idxI92I)))
(let ((valI96I _tmp_4I95I))
(let ((_tmp_10I100I (nscore__list__s_unsafe_push_t_nsmain__func_I159I lpI91I valI96I)))
(let ((_tmp_13I98I (+ idxI92I 1)))
(ite (@int_unsafe _tmp_13I98I)
(result_error@nscore__list_t_nsmain__func_I19I (result_error 2))
(let ((@tmpvar@74 (nscore__list__s_append_t_nsmain__func_I160I@gas2 lI81I lsizeI90I _tmp_10I100I _tmp_13I98I)))
(ite (is-result_error@nscore__list_t_nsmain__func_I19I @tmpvar@74)
@tmpvar@74
(let ((_tmp_7I97I (result_success_value@nscore__list_t_nsmain__func_I19I @tmpvar@74)))
(let ((___ir_ret__I66I _tmp_7I97I))
(let ((___ir_ret___2I75I ___ir_ret__I66I))
(let (($return ___ir_ret___2I75I))
(result_success@nscore__list_t_nsmain__func_I19I $return)
)
)
)
)
)
)
)
)
)
)
)
)
))
(define-fun nscore__list__s_append_t_nsmain__func_I160I@gas4 ((lI81I nscore__list_t_nsmain__func_I19I) (lsizeI90I Int) (lpI91I nscore__list_t_nsmain__func_I19I) (idxI92I Int)) Result@nscore__list_t_nsmain__func_I19I
(let ((_tmp_0I65I (= idxI92I lsizeI90I)))
(ite _tmp_0I65I
(let ((___ir_ret___1I74I lpI91I))
(let ((___ir_ret___2I75I ___ir_ret___1I74I))
(let (($return ___ir_ret___2I75I))
(result_success@nscore__list_t_nsmain__func_I19I $return)
)
)
)
(let ((_tmp_4I95I (nscore__list__s_unsafe_get_t_nsmain__func_I158I lI81I idxI92I)))
(let ((valI96I _tmp_4I95I))
(let ((_tmp_10I100I (nscore__list__s_unsafe_push_t_nsmain__func_I159I lpI91I valI96I)))
(let ((_tmp_13I98I (+ idxI92I 1)))
(ite (@int_unsafe _tmp_13I98I)
(result_error@nscore__list_t_nsmain__func_I19I (result_error 2))
(let ((@tmpvar@75 (nscore__list__s_append_t_nsmain__func_I160I@gas3 lI81I lsizeI90I _tmp_10I100I _tmp_13I98I)))
(ite (is-result_error@nscore__list_t_nsmain__func_I19I @tmpvar@75)
@tmpvar@75
(let ((_tmp_7I97I (result_success_value@nscore__list_t_nsmain__func_I19I @tmpvar@75)))
(let ((___ir_ret__I66I _tmp_7I97I))
(let ((___ir_ret___2I75I ___ir_ret__I66I))
(let (($return ___ir_ret___2I75I))
(result_success@nscore__list_t_nsmain__func_I19I $return)
)
)
)
)
)
)
)
)
)
)
)
)
))
(define-fun nscore__list__s_append_t_nsmain__func_I160I ((lI81I nscore__list_t_nsmain__func_I19I) (lsizeI90I Int) (lpI91I nscore__list_t_nsmain__func_I19I) (idxI92I Int)) Result@nscore__list_t_nsmain__func_I19I
(let ((_tmp_0I65I (= idxI92I lsizeI90I)))
(ite _tmp_0I65I
(let ((___ir_ret___1I74I lpI91I))
(let ((___ir_ret___2I75I ___ir_ret___1I74I))
(let (($return ___ir_ret___2I75I))
(result_success@nscore__list_t_nsmain__func_I19I $return)
)
)
)
(let ((_tmp_4I95I (nscore__list__s_unsafe_get_t_nsmain__func_I158I lI81I idxI92I)))
(let ((valI96I _tmp_4I95I))
(let ((_tmp_10I100I (nscore__list__s_unsafe_push_t_nsmain__func_I159I lpI91I valI96I)))
(let ((_tmp_13I98I (+ idxI92I 1)))
(ite (@int_unsafe _tmp_13I98I)
(result_error@nscore__list_t_nsmain__func_I19I (result_error 2))
(let ((@tmpvar@76 (nscore__list__s_append_t_nsmain__func_I160I@gas4 lI81I lsizeI90I _tmp_10I100I _tmp_13I98I)))
(ite (is-result_error@nscore__list_t_nsmain__func_I19I @tmpvar@76)
@tmpvar@76
(let ((_tmp_7I97I (result_success_value@nscore__list_t_nsmain__func_I19I @tmpvar@76)))
(let ((___ir_ret__I66I _tmp_7I97I))
(let ((___ir_ret___2I75I ___ir_ret__I66I))
(let (($return ___ir_ret___2I75I))
(result_success@nscore__list_t_nsmain__func_I19I $return)
)
)
)
)
)
)
)
)
)
)
)
)
))
(define-fun nscore__list__append_t_nsmain__func_I161I ((thisI79I nscore__list_t_nsmain__func_I19I) (lI81I nscore__list_t_nsmain__func_I19I)) Result@nscore__list_t_nsmain__func_I19I
(let ((_tmp_2I104I (nscore__list__s_size_t_nsmain__func_I157I lI81I)))
(let ((@tmpvar@77 (nscore__list__s_append_t_nsmain__func_I160I lI81I _tmp_2I104I thisI79I 0)))
(ite (is-result_error@nscore__list_t_nsmain__func_I19I @tmpvar@77)
@tmpvar@77
(let ((_tmp_0I65I (result_success_value@nscore__list_t_nsmain__func_I19I @tmpvar@77)))
(let ((___ir_ret__I66I _tmp_0I65I))
(let (($return ___ir_ret__I66I))
(result_success@nscore__list_t_nsmain__func_I19I $return)
)
)
)
)
)
))
(define-fun nsmain__testscheduler__uschedI163I ((thisI79I nsmain__testschedulerI34I) (delayI162I Int) (funcI111I nsmain__funcI20I)) Result@nsmain__testschedulerI34I
(let ((_tmp_3I62I (nsmain__testschedulerI34I@nsmain__testscheduler_currenttimeI36I thisI79I)))
(let ((_tmp_0I65I (+ _tmp_3I62I delayI162I)))
(ite (@int_unsafe _tmp_0I65I)
(result_error@nsmain__testschedulerI34I (result_error 5))
(let ((atI110I _tmp_0I65I))
(let ((_tmp_8I144I (nsmain__testschedulerI34I@nsmain__testscheduler_timelineI37I thisI79I)))
(let ((@tmpvar@78 (nscore__map__has_k_nscore__int__v_nscore__list_nsmain__func__I80I _tmp_8I144I atI110I)))
(ite (is-result_error@Bool @tmpvar@78)
(result_error@nsmain__testschedulerI34I (result_error_code@Bool @tmpvar@78))
(let ((_tmp_9I164I (result_success_value@Bool @tmpvar@78)))
(ite _tmp_9I164I
(let ((_tmp_14I165I (nsmain__testschedulerI34I@nsmain__testscheduler_timelineI37I thisI79I)))
(let ((@tmpvar@79 (nscore__map__keys_k_nscore__int__v_nscore__list_nsmain__func__I145I _tmp_14I165I)))
(ite (is-result_error@nscore__list_t_nscore__int_I17I @tmpvar@79)
(result_error@nsmain__testschedulerI34I (result_error_code@nscore__list_t_nscore__int_I17I @tmpvar@79))
(let ((_tmp_15I134I (result_success_value@nscore__list_t_nscore__int_I17I @tmpvar@79)))
(let ((@tmpvar@80 (nscore__list__get_t_nscore__int_I153I _tmp_15I134I atI110I)))
(ite (is-result_error@Int @tmpvar@80)
(result_error@nsmain__testschedulerI34I (result_error_code@Int @tmpvar@80))
(let ((_tmp_16I99I (result_success_value@Int @tmpvar@80)))
(let ((_tmp_20I102I (nsmain__testschedulerI34I@nsmain__testscheduler_timelineI37I thisI79I)))
(let ((@tmpvar@81 (nscore__map__get_k_nscore__int__v_nscore__list_nsmain__func__I156I _tmp_20I102I atI110I)))
(ite (is-result_error@nscore__list_t_nsmain__func_I19I @tmpvar@81)
(result_error@nsmain__testschedulerI34I (result_error_code@nscore__list_t_nsmain__func_I19I @tmpvar@81))
(let ((_tmp_21I166I (result_success_value@nscore__list_t_nsmain__func_I19I @tmpvar@81)))
(let ((_tmp_24I101I (nscore__list_t_nsmain__func_I19I@cons 1 (store nscore__list_t_nsmain__func__collection_data_array_emptyI21I 0 funcI111I))))
(let ((@tmpvar@82 (nscore__list__append_t_nsmain__func_I161I _tmp_21I166I _tmp_24I101I)))
(ite (is-result_error@nscore__list_t_nsmain__func_I19I @tmpvar@82)
(result_error@nsmain__testschedulerI34I (result_error_code@nscore__list_t_nsmain__func_I19I @tmpvar@82))
(let ((_tmp_23I167I (result_success_value@nscore__list_t_nsmain__func_I19I @tmpvar@82)))
(let ((_tmp_11I129I (nscore__mapentry_k_nscore__int__v_nscore__list_nsmain__func__I26I@cons _tmp_16I99I _tmp_23I167I)))
(let ((_tmp_5_1I168I (nscore__map_k_nscore__int__v_nscore__list_nsmain__func__I23I@cons 1 (store nscore__map_k_nscore__int__v_nscore__list_nsmain__func___collection_has_array_emptyI25I (nscore__mapentry_k_nscore__int__v_nscore__list_nsmain__func__I26I@nscore__mapentry_k_nscore__int__v_nscore__list_nsmain__func___keyI27I _tmp_11I129I) true) (store nscore__map_k_nscore__int__v_nscore__list_nsmain__func___collection_data_array_emptyI24I (nscore__mapentry_k_nscore__int__v_nscore__list_nsmain__func__I26I@nscore__mapentry_k_nscore__int__v_nscore__list_nsmain__func___keyI27I _tmp_11I129I) (nscore__mapentry_k_nscore__int__v_nscore__list_nsmain__func__I26I@nscore__mapentry_k_nscore__int__v_nscore__list_nsmain__func___valueI28I _tmp_11I129I)) (bsqterm_object MIRNominalTypeEnum_nscore__keylist_k_nscore__int_I11I (cons@bsq_object_from_nscore__keylist_k_nscore__int_I11I (nscore__keylist_k_nscore__int_I11I@cons (nscore__mapentry_k_nscore__int__v_nscore__list_nsmain__func__I26I@nscore__mapentry_k_nscore__int__v_nscore__list_nsmain__func___keyI27I _tmp_11I129I) bsqterm_none))))))
(let ((@tmpvar@83 (nsmain__testscheduler__usched__lselect_done_3I113I atI110I funcI111I thisI79I _tmp_5_1I168I)))
(ite (is-result_error@nsmain__testschedulerI34I @tmpvar@83)
@tmpvar@83
(let ((_tmp_100001I150I (result_success_value@nsmain__testschedulerI34I @tmpvar@83)))
(let (($return _tmp_100001I150I))
(result_success@nsmain__testschedulerI34I $return)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
(let ((_tmp_28I169I (nscore__list_t_nsmain__func_I19I@cons 1 (store nscore__list_t_nsmain__func__collection_data_array_emptyI21I 0 funcI111I))))
(let ((_tmp_26I136I (nscore__mapentry_k_nscore__int__v_nscore__list_nsmain__func__I26I@cons atI110I _tmp_28I169I)))
(let ((_tmp_5I63I (nscore__map_k_nscore__int__v_nscore__list_nsmain__func__I23I@cons 1 (store nscore__map_k_nscore__int__v_nscore__list_nsmain__func___collection_has_array_emptyI25I (nscore__mapentry_k_nscore__int__v_nscore__list_nsmain__func__I26I@nscore__mapentry_k_nscore__int__v_nscore__list_nsmain__func___keyI27I _tmp_26I136I) true) (store nscore__map_k_nscore__int__v_nscore__list_nsmain__func___collection_data_array_emptyI24I (nscore__mapentry_k_nscore__int__v_nscore__list_nsmain__func__I26I@nscore__mapentry_k_nscore__int__v_nscore__list_nsmain__func___keyI27I _tmp_26I136I) (nscore__mapentry_k_nscore__int__v_nscore__list_nsmain__func__I26I@nscore__mapentry_k_nscore__int__v_nscore__list_nsmain__func___valueI28I _tmp_26I136I)) (bsqterm_object MIRNominalTypeEnum_nscore__keylist_k_nscore__int_I11I (cons@bsq_object_from_nscore__keylist_k_nscore__int_I11I (nscore__keylist_k_nscore__int_I11I@cons (nscore__mapentry_k_nscore__int__v_nscore__list_nsmain__func__I26I@nscore__mapentry_k_nscore__int__v_nscore__list_nsmain__func___keyI27I _tmp_26I136I) bsqterm_none))))))
(let ((@tmpvar@84 (nsmain__testscheduler__usched__lselect_done_3I113I atI110I funcI111I thisI79I _tmp_5I63I)))
(ite (is-result_error@nsmain__testschedulerI34I @tmpvar@84)
@tmpvar@84
(let ((_tmp_100000I151I (result_success_value@nsmain__testschedulerI34I @tmpvar@84)))
(let (($return _tmp_100000I151I))
(result_success@nsmain__testschedulerI34I $return)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
))
(define-fun nsmain__testscheduler__scheduleI170I ((thisI79I nsmain__testschedulerI34I) (funcI111I nsmain__funcI20I)) Result@nsmain__testschedulerI34I
(let ((_tmp_4I95I (nsmain__testschedulerI34I@nsmain__testscheduler_currenttimeI36I thisI79I)))
(let ((@tmpvar@85 (nsmain__testscheduler__uschedI163I thisI79I _tmp_4I95I funcI111I)))
(ite (is-result_error@nsmain__testschedulerI34I @tmpvar@85)
@tmpvar@85
(let ((_tmp_0I65I (result_success_value@nsmain__testschedulerI34I @tmpvar@85)))
(let ((schI171I _tmp_0I65I))
(let ((_tmp_9I164I (nsmain__testschedulerI34I@nsmain__testscheduler_runningI38I thisI79I)))
(let ((_tmp_6I64I (not _tmp_9I164I)))
(ite _tmp_6I64I
(let ((_tmp_16I99I (nsmain__testschedulerI34I@nsmain__testscheduler_sortedtasksI40I schI171I)))
(let ((_tmp_12I131I (nsmain__testschedulerI34I@cons (nsmain__testschedulerI34I@nsmain__testscheduler_nowI35I thisI79I) (nsmain__testschedulerI34I@nsmain__testscheduler_currenttimeI36I thisI79I) (nsmain__testschedulerI34I@nsmain__testscheduler_timelineI37I thisI79I) true (nsmain__testschedulerI34I@nsmain__testscheduler_runlistI39I thisI79I) _tmp_16I99I)))
(let ((rI172I _tmp_12I131I))
(let ((___ir_ret___1I74I rI172I))
(let ((___ir_ret___2I75I ___ir_ret___1I74I))
(let (($return ___ir_ret___2I75I))
(result_success@nsmain__testschedulerI34I $return)
)
)
)
)
)
)
(let ((___ir_ret__I66I schI171I))
(let ((___ir_ret___2I75I ___ir_ret__I66I))
(let (($return ___ir_ret___2I75I))
(result_success@nsmain__testschedulerI34I $return)
)
)
)
)
)
)
)
)
)
)
))
(define-fun fn__fibersched_bsq_139__3639I173I () Result@String
(let ((___ir_ret__I66I "R2"))
(let (($return ___ir_ret__I66I))
(result_success@String $return)
)
))
(define-fun nsmain__func__enqueue_fibersched_bsq_139_0_I174I () Result@bsq_record
(let ((@tmpvar@86 fn__fibersched_bsq_139__3639I173I))
(ite (is-result_error@String @tmpvar@86)
(result_error@bsq_record (result_error_code@String @tmpvar@86))
(let ((_tmp_1I69I (result_success_value@String @tmpvar@86)))
(let ((_tmp_0I65I (bsq_record@cons (StructuralSpecialTypeInfo@cons false true true) (store bsqrecord_array_empty "lf" (bsqterm_key (bsqkey_string _tmp_1I69I))))))
(let ((___ir_ret__I66I _tmp_0I65I))
(let (($return ___ir_ret__I66I))
(result_success@bsq_record $return)
)
)
)
)
)
))
(define-fun nsmain__testscheduler__delayI176I ((thisI79I nsmain__testschedulerI34I) (timeoutI175I Int) (funcI111I nsmain__funcI20I)) Result@nsmain__testschedulerI34I
(let ((@tmpvar@87 (nsmain__testscheduler__uschedI163I thisI79I timeoutI175I funcI111I)))
(ite (is-result_error@nsmain__testschedulerI34I @tmpvar@87)
@tmpvar@87
(let ((_tmp_0I65I (result_success_value@nsmain__testschedulerI34I @tmpvar@87)))
(let ((schI171I _tmp_0I65I))
(let ((___ir_ret__I66I schI171I))
(let (($return ___ir_ret__I66I))
(result_success@nsmain__testschedulerI34I $return)
)
)
)
)
)
))
(define-fun fn__fibersched_bsq_140__3685I177I () Result@String
(let ((___ir_ret__I66I "R3"))
(let (($return ___ir_ret__I66I))
(result_success@String $return)
)
))
(define-fun nsmain__func__enqueue_fibersched_bsq_140_0_I178I () Result@bsq_record
(let ((@tmpvar@88 fn__fibersched_bsq_140__3685I177I))
(ite (is-result_error@String @tmpvar@88)
(result_error@bsq_record (result_error_code@String @tmpvar@88))
(let ((_tmp_1I69I (result_success_value@String @tmpvar@88)))
(let ((_tmp_0I65I (bsq_record@cons (StructuralSpecialTypeInfo@cons false true true) (store bsqrecord_array_empty "lf" (bsqterm_key (bsqkey_string _tmp_1I69I))))))
(let ((___ir_ret__I66I _tmp_0I65I))
(let (($return ___ir_ret__I66I))
(result_success@bsq_record $return)
)
)
)
)
)
))
(define-fun nscore__map__s_size_k_nscore__int__v_nscore__list_nsmain__func__I179I ((mI76I nscore__map_k_nscore__int__v_nscore__list_nsmain__func__I23I)) Int
(nscore__map_k_nscore__int__v_nscore__list_nsmain__func__I23I@@size mI76I)
)
(define-fun nscore__map__empty_k_nscore__int__v_nscore__list_nsmain__func__I180I ((thisI79I nscore__map_k_nscore__int__v_nscore__list_nsmain__func__I23I)) Result@Bool
(let ((_tmp_1I69I (nscore__map__s_size_k_nscore__int__v_nscore__list_nsmain__func__I179I thisI79I)))
(let ((_tmp_0I65I (= _tmp_1I69I 0)))
(let ((___ir_ret__I66I _tmp_0I65I))
(let (($return ___ir_ret__I66I))
(result_success@Bool $return)
)
)
)
))
(define-fun nsmain__testscheduler__runI181I ((thisI79I nsmain__testschedulerI34I)) Result@nsmain__testschedulerI34I
(let ((_tmp_2I104I (nsmain__testschedulerI34I@nsmain__testscheduler_timelineI37I thisI79I)))
(let ((@tmpvar@89 (nscore__map__empty_k_nscore__int__v_nscore__list_nsmain__func__I180I _tmp_2I104I)))
(ite (is-result_error@Bool @tmpvar@89)
(result_error@nsmain__testschedulerI34I (result_error_code@Bool @tmpvar@89))
(let ((_tmp_3I62I (result_success_value@Bool @tmpvar@89)))
(ite _tmp_3I62I
(let ((_tmp_6I64I (nsmain__testschedulerI34I@cons (nsmain__testschedulerI34I@nsmain__testscheduler_nowI35I thisI79I) (nsmain__testschedulerI34I@nsmain__testscheduler_currenttimeI36I thisI79I) (nsmain__testschedulerI34I@nsmain__testscheduler_timelineI37I thisI79I) false (nsmain__testschedulerI34I@nsmain__testscheduler_runlistI39I thisI79I) (nsmain__testschedulerI34I@nsmain__testscheduler_sortedtasksI40I thisI79I))))
(let ((___ir_ret___1I74I _tmp_6I64I))
(let ((___ir_ret___2I75I ___ir_ret___1I74I))
(let (($return ___ir_ret___2I75I))
(result_success@nsmain__testschedulerI34I $return)
)
)
)
)
(let ((_tmp_13I98I (nsmain__testschedulerI34I@nsmain__testscheduler_nowI35I thisI79I)))
(let ((_tmp_16I99I (nsmain__testschedulerI34I@nsmain__testscheduler_sortedtasksI40I thisI79I)))
(let ((_tmp_17I140I (nscore__list_t__func_nsmain__func__time_nscore__int__I15I@cons 0 nscore__list_t__func_nsmain__func__time_nscore__int___collection_data_array_emptyI16I)))
(let ((_tmp_10I100I (nsmain__testschedulerI34I@cons (nsmain__testschedulerI34I@nsmain__testscheduler_nowI35I thisI79I) _tmp_13I98I (nsmain__testschedulerI34I@nsmain__testscheduler_timelineI37I thisI79I) (nsmain__testschedulerI34I@nsmain__testscheduler_runningI38I thisI79I) _tmp_16I99I _tmp_17I140I)))
(let ((rI172I _tmp_10I100I))
(let ((___ir_ret__I66I rI172I))
(let ((___ir_ret___2I75I ___ir_ret__I66I))
(let (($return ___ir_ret___2I75I))
(result_success@nsmain__testschedulerI34I $return)
)
)
)
)
)
)
)
)
)
)
)
)
))
(define-fun nsmain__testscheduler__utcnowI182I ((thisI79I nsmain__testschedulerI34I)) Result@Int
(let ((_tmp_2I104I (nsmain__testschedulerI34I@nsmain__testscheduler_currenttimeI36I thisI79I)))
(let ((___ir_ret__I66I _tmp_2I104I))
(let (($return ___ir_ret__I66I))
(result_success@Int $return)
)
)
))
(define-fun nscore__list__get_t__func_nsmain__func__time_nscore__int____pre__llogic_done_3I183I ((_tmp_0_2I146I Bool)) Result@Bool
(let ((___ir_ret__I66I _tmp_0_2I146I))
(let (($return ___ir_ret__I66I))
(result_success@Bool $return)
)
))
(define-fun nscore__list__get_t__func_nsmain__func__time_nscore__int____preI184I ((thisI79I nscore__list_t__func_nsmain__func__time_nscore__int__I15I) (iI83I Int)) Result@Bool
(let ((_tmp_1I69I (or (< 0 iI83I) (= 0 iI83I))))
(ite _tmp_1I69I
(let ((_tmp_6I64I (nscore__list__s_size_t__func_nsmain__func__time_nscore__int__I82I thisI79I)))
(let ((_tmp_4I95I (< iI83I _tmp_6I64I)))
(let ((_tmp_0_1I73I _tmp_4I95I))
(let ((@tmpvar@90 (nscore__list__get_t__func_nsmain__func__time_nscore__int____pre__llogic_done_3I183I _tmp_0_1I73I)))
(ite (is-result_error@Bool @tmpvar@90)
@tmpvar@90
(let ((_tmp_100001I150I (result_success_value@Bool @tmpvar@90)))
(let (($return _tmp_100001I150I))
(result_success@Bool $return)
)
)
)
)
)
)
)
(let ((_tmp_0I65I false))
(let ((@tmpvar@91 (nscore__list__get_t__func_nsmain__func__time_nscore__int____pre__llogic_done_3I183I _tmp_0I65I)))
(ite (is-result_error@Bool @tmpvar@91)
@tmpvar@91
(let ((_tmp_100000I151I (result_success_value@Bool @tmpvar@91)))
(let (($return _tmp_100000I151I))
(result_success@Bool $return)
)
)
)
)
)
)
))
(define-fun nscore__list__get_t__func_nsmain__func__time_nscore__int__I185I ((thisI79I nscore__list_t__func_nsmain__func__time_nscore__int__I15I) (iI83I Int)) Result@bsq_record
(let ((@tmpvar@92 (nscore__list__get_t__func_nsmain__func__time_nscore__int____preI184I thisI79I iI83I)))
(ite (is-result_error@Bool @tmpvar@92)
(result_error@bsq_record (result_error_code@Bool @tmpvar@92))
(let ((_tmp_0I65I (result_success_value@Bool @tmpvar@92)))
(ite _tmp_0I65I
(let ((_tmp_1I69I (nscore__list__s_unsafe_get_t__func_nsmain__func__time_nscore__int__I84I thisI79I iI83I)))
(let ((___ir_ret__I66I _tmp_1I69I))
(let (($return ___ir_ret__I66I))
(result_success@bsq_record $return)
)
)
)
(result_error@bsq_record (result_error 3))
)
)
)
))
(define-fun nsmain__func__exeI186I ((thisI79I nsmain__funcI20I)) Result@String
(let ((_tmp_2I104I (nsmain__funcI20I@nsmain__func_lfI33I thisI79I)))
(let ((___ir_ret__I66I _tmp_2I104I))
(let (($return ___ir_ret__I66I))
(result_success@String $return)
)
)
))
(define-fun nsmain__mainI187I () Result@BTerm
(let ((@tmpvar@93 nsmain__testscheduler__newI61I))
(ite (is-result_error@bsq_record @tmpvar@93)
(result_error@BTerm (result_error_code@bsq_record @tmpvar@93))
(let ((_tmp_2I104I (result_success_value@bsq_record @tmpvar@93)))
(let ((_tmp_3I62I (bsqkey_int_value (bsqterm_key_value (select (bsq_record_entries _tmp_2I104I) "currentTime")))))
(let ((_tmp_4I95I (bsqkey_int_value (bsqterm_key_value (select (bsq_record_entries _tmp_2I104I) "now")))))
(let ((_tmp_5I63I (bsqterm_object_nscore__list_t__func_nsmain__func__time_nscore__int__I15I_value (bsqterm_object_value (select (bsq_record_entries _tmp_2I104I) "runlist")))))
(let ((_tmp_6I64I (bsqkey_bool_value (bsqterm_key_value (select (bsq_record_entries _tmp_2I104I) "running")))))
(let ((_tmp_7I97I (bsqterm_object_nscore__list_t__func_nsmain__func__time_nscore__int__I15I_value (bsqterm_object_value (select (bsq_record_entries _tmp_2I104I) "sortedTasks")))))
(let ((_tmp_8I144I (bsqterm_object_nscore__map_k_nscore__int__v_nscore__list_nsmain__func__I23I_value (bsqterm_object_value (select (bsq_record_entries _tmp_2I104I) "timeline")))))
(let ((_tmp_1I69I (nsmain__testschedulerI34I@cons _tmp_4I95I _tmp_3I62I _tmp_8I144I _tmp_6I64I _tmp_5I63I _tmp_7I97I)))
(let ((@tmpvar@94 nsmain__func__enqueue_fibersched_bsq_138_0_I68I))
(ite (is-result_error@bsq_record @tmpvar@94)
(result_error@BTerm (result_error_code@bsq_record @tmpvar@94))
(let ((_tmp_12I131I (result_success_value@bsq_record @tmpvar@94)))
(let ((_tmp_13I98I (bsqkey_string_value (bsqterm_key_value (select (bsq_record_entries _tmp_12I131I) "lf")))))
(let ((_tmp_10I100I (nsmain__funcI20I@cons _tmp_13I98I)))
(let ((@tmpvar@95 (nsmain__func____invariantI72I (nsmain__funcI20I@nsmain__func_lfI33I _tmp_10I100I))))
(ite (is-result_error@Bool @tmpvar@95)
(result_error@BTerm (result_error_code@Bool @tmpvar@95))
(let ((_tmp_14I165I (result_success_value@Bool @tmpvar@95)))
(ite _tmp_14I165I
(let ((@tmpvar@96 (nsmain__testscheduler__scheduleI170I _tmp_1I69I _tmp_10I100I)))
(ite (is-result_error@nsmain__testschedulerI34I @tmpvar@96)
(result_error@BTerm (result_error_code@nsmain__testschedulerI34I @tmpvar@96))
(let ((_tmp_9I164I (result_success_value@nsmain__testschedulerI34I @tmpvar@96)))
(let ((_tmp_16I99I 18))
(let ((@tmpvar@97 nsmain__func__enqueue_fibersched_bsq_139_0_I174I))
(ite (is-result_error@bsq_record @tmpvar@97)
(result_error@BTerm (result_error_code@bsq_record @tmpvar@97))
(let ((_tmp_19I133I (result_success_value@bsq_record @tmpvar@97)))
(let ((_tmp_20I102I (bsqkey_string_value (bsqterm_key_value (select (bsq_record_entries _tmp_19I133I) "lf")))))
(let ((_tmp_17I140I (nsmain__funcI20I@cons _tmp_20I102I)))
(let ((@tmpvar@98 (nsmain__func____invariantI72I (nsmain__funcI20I@nsmain__func_lfI33I _tmp_17I140I))))
(ite (is-result_error@Bool @tmpvar@98)
(result_error@BTerm (result_error_code@Bool @tmpvar@98))
(let ((_tmp_21I166I (result_success_value@Bool @tmpvar@98)))
(ite _tmp_21I166I
(let ((@tmpvar@99 (nsmain__testscheduler__delayI176I _tmp_9I164I _tmp_16I99I _tmp_17I140I)))
(ite (is-result_error@nsmain__testschedulerI34I @tmpvar@99)
(result_error@BTerm (result_error_code@nsmain__testschedulerI34I @tmpvar@99))
(let ((_tmp_15I134I (result_success_value@nsmain__testschedulerI34I @tmpvar@99)))
(let ((_tmp_23I167I 2))
(let ((@tmpvar@100 nsmain__func__enqueue_fibersched_bsq_140_0_I178I))
(ite (is-result_error@bsq_record @tmpvar@100)
(result_error@BTerm (result_error_code@bsq_record @tmpvar@100))
(let ((_tmp_26I136I (result_success_value@bsq_record @tmpvar@100)))
(let ((_tmp_27I188I (bsqkey_string_value (bsqterm_key_value (select (bsq_record_entries _tmp_26I136I) "lf")))))
(let ((_tmp_24I101I (nsmain__funcI20I@cons _tmp_27I188I)))
(let ((@tmpvar@101 (nsmain__func____invariantI72I (nsmain__funcI20I@nsmain__func_lfI33I _tmp_24I101I))))
(ite (is-result_error@Bool @tmpvar@101)
(result_error@BTerm (result_error_code@Bool @tmpvar@101))
(let ((_tmp_28I169I (result_success_value@Bool @tmpvar@101)))
(ite _tmp_28I169I
(let ((@tmpvar@102 (nsmain__testscheduler__delayI176I _tmp_15I134I _tmp_23I167I _tmp_24I101I)))
(ite (is-result_error@nsmain__testschedulerI34I @tmpvar@102)
(result_error@BTerm (result_error_code@nsmain__testschedulerI34I @tmpvar@102))
(let ((_tmp_22I137I (result_success_value@nsmain__testschedulerI34I @tmpvar@102)))
(let ((@tmpvar@103 (nsmain__testscheduler__runI181I _tmp_22I137I)))
(ite (is-result_error@nsmain__testschedulerI34I @tmpvar@103)
(result_error@BTerm (result_error_code@nsmain__testschedulerI34I @tmpvar@103))
(let ((_tmp_29I189I (result_success_value@nsmain__testschedulerI34I @tmpvar@103)))
(let ((sI190I _tmp_29I189I))
(let ((@tmpvar@104 (nsmain__testscheduler__utcnowI182I sI190I)))
(ite (is-result_error@Int @tmpvar@104)
(result_error@BTerm (result_error_code@Int @tmpvar@104))
(let ((_tmp_30I191I (result_success_value@Int @tmpvar@104)))
(let ((currenttimeI192I _tmp_30I191I))
(let ((_tmp_36I193I (nsmain__testschedulerI34I@nsmain__testscheduler_nowI35I sI190I)))
(let ((_tmp_32I115I (= currenttimeI192I _tmp_36I193I)))
(ite _tmp_32I115I
(let ((_tmp_40I194I (nsmain__testschedulerI34I@nsmain__testscheduler_runlistI39I sI190I)))
(let ((@tmpvar@105 (nscore__list__get_t__func_nsmain__func__time_nscore__int__I185I _tmp_40I194I 0)))
(ite (is-result_error@bsq_record @tmpvar@105)
(result_error@BTerm (result_error_code@bsq_record @tmpvar@105))
(let ((_tmp_41I195I (result_success_value@bsq_record @tmpvar@105)))
(let ((_tmp_43I196I (bsqterm_object_nsmain__funcI20I_value (bsqterm_object_value (select (bsq_record_entries _tmp_41I195I) "func")))))
(let ((@tmpvar@106 (nsmain__func__exeI186I _tmp_43I196I)))
(ite (is-result_error@String @tmpvar@106)
(result_error@BTerm (result_error_code@String @tmpvar@106))
(let ((_tmp_44I197I (result_success_value@String @tmpvar@106)))
(let ((_tmp_37I118I (= _tmp_44I197I "R1")))
(ite _tmp_37I118I
(let ((_tmp_49I198I (nsmain__testschedulerI34I@nsmain__testscheduler_runlistI39I sI190I)))
(let ((@tmpvar@107 (nscore__list__get_t__func_nsmain__func__time_nscore__int__I185I _tmp_49I198I 1)))
(ite (is-result_error@bsq_record @tmpvar@107)
(result_error@BTerm (result_error_code@bsq_record @tmpvar@107))
(let ((_tmp_50I124I (result_success_value@bsq_record @tmpvar@107)))
(let ((_tmp_52I199I (bsqterm_object_nsmain__funcI20I_value (bsqterm_object_value (select (bsq_record_entries _tmp_50I124I) "func")))))
(let ((@tmpvar@108 (nsmain__func__exeI186I _tmp_52I199I)))
(ite (is-result_error@String @tmpvar@108)
(result_error@BTerm (result_error_code@String @tmpvar@108))
(let ((_tmp_53I200I (result_success_value@String @tmpvar@108)))
(let ((_tmp_46I122I (= _tmp_53I200I "R3")))
(ite _tmp_46I122I
(let ((_tmp_58I201I (nsmain__testschedulerI34I@nsmain__testscheduler_runlistI39I sI190I)))
(let ((@tmpvar@109 (nscore__list__get_t__func_nsmain__func__time_nscore__int__I185I _tmp_58I201I 2)))
(ite (is-result_error@bsq_record @tmpvar@109)
(result_error@BTerm (result_error_code@bsq_record @tmpvar@109))
(let ((_tmp_59I202I (result_success_value@bsq_record @tmpvar@109)))
(let ((_tmp_61I203I (bsqterm_object_nsmain__funcI20I_value (bsqterm_object_value (select (bsq_record_entries _tmp_59I202I) "func")))))
(let ((@tmpvar@110 (nsmain__func__exeI186I _tmp_61I203I)))
(ite (is-result_error@String @tmpvar@110)
(result_error@BTerm (result_error_code@String @tmpvar@110))
(let ((_tmp_62I204I (result_success_value@String @tmpvar@110)))
(let ((_tmp_55I205I (= _tmp_62I204I "R2")))
(ite _tmp_55I205I
(let ((_tmp_67I206I (nsmain__testschedulerI34I@nsmain__testscheduler_runlistI39I sI190I)))
(let ((_tmp_64I207I (bsq_tuple@cons (StructuralSpecialTypeInfo@cons false false false) (store (store bsqtuple_array_empty 0 (bsqterm_object MIRNominalTypeEnum_nscore__list_t__func_nsmain__func__time_nscore__int__I15I (cons@bsq_object_from_nscore__list_t__func_nsmain__func__time_nscore__int__I15I _tmp_67I206I))) 1 (bsqterm_key (bsqkey_int currenttimeI192I))))))
(let ((___ir_ret__I66I _tmp_64I207I))
(let (($return (bsqterm_tuple ___ir_ret__I66I)))
(result_success@BTerm $return)
)
)
)
)
(result_error@BTerm (result_error 6))
)
)
)
)
)
)
)
)
)
)
(result_error@BTerm (result_error 7))
)
)
)
)
)
)
)
)
)
)
(result_error@BTerm (result_error 8))
)
)
)
)
)
)
)
)
)
)
(result_error@BTerm (result_error 9))
)
)
)
)
)
)
)
)
)
)
)
)
)
)
(result_error@BTerm (result_error 10))
)
)
)
)
)
)
)
)
)
)
)
)
)
(result_error@BTerm (result_error 11))
)
)
)
)
)
)
)
)
)
)
)
)
)
(result_error@BTerm (result_error 12))
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
))
(declare-const @smtres@ Result@BTerm)
(assert (= @smtres@ nsmain__mainI187I))
(assert (not (and (is-result_error@BTerm @smtres@) (is-result_bmc (result_error_code@BTerm @smtres@)))))
(assert (is-result_error@BTerm @smtres@))
(check-sat)
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Symbolic testing of Bosque sources in files:
fibersched.bsq
...
Transpiling Bosque assembly to bytecode with entrypoint of NSMain::main...
Running z3 on SMT encoding...
Writing SMT output to "fibersched.smt2..."
(simplifier :num-exprs 2800 :num-asts 88663 :time 0.00 :before-memory 38.52 :after-memory 38.72)
(simplifier :num-exprs 2800 :num-asts 88473 :time 0.00 :before-memory 38.61 :after-memory 38.61)
(propagate-values :num-exprs 2381 :num-asts 88266 :time 0.00 :before-memory 38.61 :after-memory 39.43)
(ctx-simplify :num-steps 30870)
(ctx-simplify :num-exprs 2513 :num-asts 88752 :time 0.00 :before-memory 39.43 :after-memory 40.86)
(simplifier :num-exprs 2513 :num-asts 88575 :time 0.00 :before-memory 39.44 :after-memory 39.44)
(solve_eqs :num-exprs 1 :num-asts 88645 :time 0.00 :before-memory 39.44 :after-memory 39.44)
unsat
Verified up to bound -- no errors found!