ProveSMTLemmasTest
|
100%
successful |
Tests
| Test | Method name | Duration | Result |
|---|---|---|---|
| [10] wellFormed.dl, \forall Heap h; \forall Object o; \forall Field f; (wellFormed(h) -> boolean::select(h, (java.lang.Object::select(h, o, f))<<Trigger>>, java.lang.Object::<created>) = TRUE | (java.lang.Object::select(h, o, f)) = null) | testSMTLemmaSoundness(String, String)[10] | 2.752s | passed |
| [11] jdiv.dl, \forall int divNum; \forall int divDenom; jdiv(divNum,divDenom) = \if (divNum >= 0) \then (div(divNum,divDenom)) \else (div(divNum*(-1),divDenom)*(-1)) | testSMTLemmaSoundness(String, String)[11] | 2.719s | passed |
| [12] empty.dl, \forall Object o; \forall Field f; ( elementOf(o,f,empty)<<Trigger>> <-> false ) | testSMTLemmaSoundness(String, String)[12] | 2.736s | passed |
| [13] allLocs.dl, \forall Object o; \forall Field f; ( elementOf(o,f,allLocs)<<Trigger>> <-> true ) | testSMTLemmaSoundness(String, String)[13] | 2.735s | passed |
| [14] arrayRange.dl, \forall Object o; \forall Object o2; \forall Field f; \forall int lo; \forall int hi; (elementOf(o,f, arrayRange(o2, lo, hi))<<Trigger>> <-> o = o2 & \exists int iv; (f = arr(iv) & lo <= iv & iv <= hi)) | testSMTLemmaSoundness(String, String)[14] | 2.705s | passed |
| [15] seqConcat.dl, \forall int i; \forall Seq s1; \forall Seq s2; ( 0 <= i & i < seqLen(s1) + seqLen(s2) -> any::seqGet(seqConcat(s1, s2), i) = \if (i < seqLen(s1)) \then (any::seqGet(s1, i)) \else (any::seqGet(s2, i-seqLen(s1)))) | testSMTLemmaSoundness(String, String)[15] | 2.751s | passed |
| [16] seqLen.dl, \forall Seq s; seqLen(s)<<Trigger>> >= 0 | testSMTLemmaSoundness(String, String)[16] | 2.711s | passed |
| [17] length.dl, \forall Object o; length(o) >= 0 | testSMTLemmaSoundness(String, String)[17] | 2.735s | passed |
| [18] freshLocs.dl, \forall Heap h; \forall Object o; \forall Field f; ( elementOf(o,f,freshLocs(h))<<Trigger>> <-> o != null & !boolean::select(h,o,java.lang.Object::<created>)=TRUE ) | testSMTLemmaSoundness(String, String)[18] | 2.704s | passed |
| [19] anon.dl, \forall Heap h; \forall Object o; \forall Field f; \forall Heap h2; \forall LocSet ls; any::select(anon(h, ls, h2), o, f)<<Trigger>> = \if(elementOf(o, f, ls) & f != java.lang.Object::<created> | elementOf(o, f, freshLocs(h))) \then(any::select(h2, o, f)) \else(any::select(h, o, f)) | testSMTLemmaSoundness(String, String)[19] | 2.752s | passed |
| [1] jmod.dl, \forall int divNum; \forall int divDenom; jmod(divNum,divDenom) = divNum + jdiv(divNum,divDenom)*(-1)*divDenom | testSMTLemmaSoundness(String, String)[1] | 2.692s | passed |
| [20] memset.dl, \forall Heap h; \forall LocSet s; \forall any x; \forall Object o; \forall Field f; any::select(memset(h, s, x), o, f)<<Trigger>> = \if(elementOf(o, f, s) & f != java.lang.Object::<created>) \then(x) \else(any::select(h, o, f)) | testSMTLemmaSoundness(String, String)[20] | 2.751s | passed |
| [21] store.dl, \forall Heap h; \forall Object o; \forall Field f; \forall Object o2; \forall Field f2; \forall any v; any::select(store(h,o,f,v), o2, f2)<<Trigger>> = \if(o = o2 & f = f2 & f != java.lang.Object::<created>) \then(v) \else(any::select(h, o2, f2)) | testSMTLemmaSoundness(String, String)[21] | 2.720s | passed |
| [22] seqSub.dl.2, \forall Seq seq; \forall int from; \forall int to; seqLen(seqSub(seq, from, to)<<Trigger>>) = \if(from < to)\then(to - from)\else(0) | testSMTLemmaSoundness(String, String)[22] | 2.736s | passed |
| [23] seqSingleton.dl, \forall any x; any::seqGet(seqSingleton(x)<<Trigger>>, 0) = x | testSMTLemmaSoundness(String, String)[23] | 2.735s | passed |
| [24] seqSingleton.dl.2, \forall any x; seqLen(seqSingleton(x)<<Trigger>>) = 1 | testSMTLemmaSoundness(String, String)[24] | 2.720s | passed |
| [25] null.dl, \forall any x; ((Null::instance(x))<<Trigger>> = TRUE -> x = null) | testSMTLemmaSoundness(String, String)[25] | 2.719s | passed |
| [2] seqSub.dl, \forall Seq seq; \forall int from; \forall int to; \forall int idx; any::seqGet(seqSub(seq, from, to)<<Trigger>>, idx) = \if(0 <= idx & idx < (to - from)) \then(any::seqGet(seq, idx + from)) \else(seqGetOutside) | testSMTLemmaSoundness(String, String)[2] | 2.716s | passed |
| [3] seqGetOutside.dl, \forall int i; \forall Seq s; ( i < 0 | i >= seqLen(s) -> any::seqGet(s, i)<<Trigger>> = seqGetOutside ) | testSMTLemmaSoundness(String, String)[3] | 2.751s | passed |
| [4] singleton.dl, \forall Object o; \forall Field f; \forall Object o2; \forall Field f2; ( elementOf(o,f, singleton(o2,f2))<<Trigger>> <-> o = o2 & f = f2 ) | testSMTLemmaSoundness(String, String)[4] | 2.735s | passed |
| [5] create.dl, \forall Heap h; \forall Object o; \forall Object o2; \forall Field f; any::select(create(h, o), o2, f)<<Trigger>> = \if(o = o2 & o != null & f = java.lang.Object::<created>) \then(TRUE) \else(any::select(h, o2, f)) | testSMTLemmaSoundness(String, String)[5] | 2.705s | passed |
| [6] allFields.dl, \forall Object o; \forall Field f; \forall Object o2; ( elementOf(o,f, allFields(o2))<<Trigger>> <-> o = o2 ) | testSMTLemmaSoundness(String, String)[6] | 2.736s | passed |
| [7] seqEmpty.dl, seqLen(seqEmpty) = 0 | testSMTLemmaSoundness(String, String)[7] | 2.750s | passed |
| [8] union.dl, \forall Object o; \forall Field f; \forall LocSet l1; \forall LocSet l2; ( elementOf(o, f, union(l1, l2))<<Trigger>> <-> elementOf(o,f,l1) | elementOf(o,f,l2) ) | testSMTLemmaSoundness(String, String)[8] | 2.719s | passed |
| [9] seqConcat.dl.2, \forall Seq s1; \forall Seq s2; seqLen(seqConcat(s1,s2)<<Trigger>>) = seqLen(s1) + seqLen(s2) | testSMTLemmaSoundness(String, String)[9] | 2.736s | passed |
Standard output
664356 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file D:\a\key\key\key.core\build\resources\test\de\uka\ilkd\key\smt\newsmt2\SMT_lemma_jmod.dl.proof 664371 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from D:\a\key\key\key.core\build\resources\test\de\uka\ilkd\key\smt\newsmt2\SMT_lemma_jmod.dl.proof 664371 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.6ns 664371 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 666920 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 666936 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jmod.dl.proof 666952 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.53ms 667061 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_1077418343782425787.key 667061 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_1077418343782425787.key 667061 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 219.7ns 667061 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 669641 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.57s 669656 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl_1077418343782425787.key 669656 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.6ns 669766 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file D:\a\key\key\key.core\build\resources\test\de\uka\ilkd\key\smt\newsmt2\SMT_lemma_seqGetOutside.dl.proof 669766 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from D:\a\key\key\key.core\build\resources\test\de\uka\ilkd\key\smt\newsmt2\SMT_lemma_seqGetOutside.dl.proof 669766 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 359ns 669766 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 672361 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.6s 672376 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqGetOutside.dl.proof 672408 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.08ms 672517 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_5009445171183263850.key 672517 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_5009445171183263850.key 672517 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 229.3ns 672517 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 675128 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.61s 675143 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_singleton.dl_5009445171183263850.key 675143 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.5ns 675253 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_10870990298244769686.key 675253 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_10870990298244769686.key 675253 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 213.6ns 675253 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 677833 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.58s 677849 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_create.dl_10870990298244769686.key 677849 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.5ns 677958 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_5704531396329364498.key 677958 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_5704531396329364498.key 677958 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 148.3ns 677958 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 680568 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.61s 680584 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allFields.dl_5704531396329364498.key 680584 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.9ns 680694 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_13613784141680551300.key 680694 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_13613784141680551300.key 680694 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 217.4ns 680694 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 683319 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.62s 683319 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqEmpty.dl_13613784141680551300.key 683335 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.2ns 683444 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_4059735529299493189.key 683444 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_4059735529299493189.key 683444 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 142.1ns 683444 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 686039 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.59s 686055 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_union.dl_4059735529299493189.key 686055 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.4ns 686164 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl.2_504211272428566670.key 686164 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl.2_504211272428566670.key 686164 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 144.4ns 686164 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 688775 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.61s 688791 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl.2_504211272428566670.key 688791 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.9ns 688900 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_4528746457730558942.key 688900 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_4528746457730558942.key 688900 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 217ns 688900 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 691526 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.62s 691541 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_wellFormed.dl_4528746457730558942.key 691541 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.5ns 691652 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file D:\a\key\key\key.core\build\resources\test\de\uka\ilkd\key\smt\newsmt2\SMT_lemma_jdiv.dl.proof 691652 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from D:\a\key\key\key.core\build\resources\test\de\uka\ilkd\key\smt\newsmt2\SMT_lemma_jdiv.dl.proof 691652 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 161.3ns 691652 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 694246 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.59s 694246 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jdiv.dl.proof 694261 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.12ms 694371 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_9267942558695494115.key 694371 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_9267942558695494115.key 694371 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 384.8ns 694371 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 696983 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.61s 696999 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_empty.dl_9267942558695494115.key 696999 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.4ns 697108 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_6241119754138055521.key 697108 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_6241119754138055521.key 697108 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 393.7ns 697108 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 699719 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.61s 699734 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allLocs.dl_6241119754138055521.key 699734 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.4ns 699844 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_10471189863823981797.key 699844 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_10471189863823981797.key 699844 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 372.7ns 699844 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 702424 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.58s 702440 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_arrayRange.dl_10471189863823981797.key 702440 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.8ns 702549 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_15172526678819663408.key 702549 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_15172526678819663408.key 702549 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 322.5ns 702549 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 705160 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.62s 705176 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl_15172526678819663408.key 705176 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.9ns 705301 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_9539993561959183078.key 705301 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_9539993561959183078.key 705301 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 329ns 705301 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 707897 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.6s 707912 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqLen.dl_9539993561959183078.key 707912 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.1ns 708013 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_8669616189295127768.key 708013 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_8669616189295127768.key 708013 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 220.5ns 708013 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 710623 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.61s 710639 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_length.dl_8669616189295127768.key 710639 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.2ns 710748 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_18305451923346503631.key 710748 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_18305451923346503631.key 710748 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 324.6ns 710748 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 713327 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.58s 713343 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_freshLocs.dl_18305451923346503631.key 713343 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.5ns 713453 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_12396546177464788476.key 713453 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_12396546177464788476.key 713453 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 376.5ns 713453 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 716079 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.62s 716095 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_anon.dl_12396546177464788476.key 716095 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.3ns 716204 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_1477391989661115386.key 716204 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_1477391989661115386.key 716204 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 396.1ns 716204 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 718832 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.62s 718832 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_memset.dl_1477391989661115386.key 718847 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.2ns 718957 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_7877032669355755527.key 718957 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_7877032669355755527.key 718957 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 356ns 718957 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 721553 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.59s 721568 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_store.dl_7877032669355755527.key 721568 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.9ns 721678 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl.2_17447738452106226478.key 721678 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl.2_17447738452106226478.key 721678 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 358.1ns 721678 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 724288 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.62s 724304 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl.2_17447738452106226478.key 724304 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.9ns 724413 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_420033727129701730.key 724413 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_420033727129701730.key 724413 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 211.9ns 724413 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 727024 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.62s 727040 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl_420033727129701730.key 727040 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.6ns 727149 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl.2_14652506605794644968.key 727149 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl.2_14652506605794644968.key 727149 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 347.4ns 727149 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 729744 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.59s 729760 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl.2_14652506605794644968.key 729760 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.4ns 729869 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_11565594014321023565.key 729869 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_11565594014321023565.key 729869 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 205.4ns 729869 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 732464 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.6s 732480 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_null.dl_11565594014321023565.key 732480 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.5ns