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] | 3.079s | 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] | 3.221s | passed |
| [12] empty.dl, \forall Object o; \forall Field f; ( elementOf(o,f,empty)<<Trigger>> <-> false ) | testSMTLemmaSoundness(String, String)[12] | 3.128s | passed |
| [13] allLocs.dl, \forall Object o; \forall Field f; ( elementOf(o,f,allLocs)<<Trigger>> <-> true ) | testSMTLemmaSoundness(String, String)[13] | 3.049s | 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] | 3.157s | 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] | 3.144s | passed |
| [16] seqLen.dl, \forall Seq s; seqLen(s)<<Trigger>> >= 0 | testSMTLemmaSoundness(String, String)[16] | 3.173s | passed |
| [17] length.dl, \forall Object o; length(o) >= 0 | testSMTLemmaSoundness(String, String)[17] | 3.361s | 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] | 3.439s | 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] | 3.284s | passed |
| [1] jmod.dl, \forall int divNum; \forall int divDenom; jmod(divNum,divDenom) = divNum + jdiv(divNum,divDenom)*(-1)*divDenom | testSMTLemmaSoundness(String, String)[1] | 3.456s | 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] | 3.330s | 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] | 3.299s | 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] | 3.331s | passed |
| [23] seqSingleton.dl, \forall any x; any::seqGet(seqSingleton(x)<<Trigger>>, 0) = x | testSMTLemmaSoundness(String, String)[23] | 3.266s | passed |
| [24] seqSingleton.dl.2, \forall any x; seqLen(seqSingleton(x)<<Trigger>>) = 1 | testSMTLemmaSoundness(String, String)[24] | 3.314s | passed |
| [25] null.dl, \forall any x; ((Null::instance(x))<<Trigger>> = TRUE -> x = null) | testSMTLemmaSoundness(String, String)[25] | 3.316s | 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] | 3.347s | 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] | 3.378s | 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] | 3.267s | 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] | 3.253s | 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] | 3.189s | passed |
| [7] seqEmpty.dl, seqLen(seqEmpty) = 0 | testSMTLemmaSoundness(String, String)[7] | 3.158s | 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] | 3.190s | passed |
| [9] seqConcat.dl.2, \forall Seq s1; \forall Seq s2; seqLen(seqConcat(s1,s2)<<Trigger>>) = seqLen(s1) + seqLen(s2) | testSMTLemmaSoundness(String, String)[9] | 3.080s | passed |
Standard output
786455 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 786455 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 786455 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 97.8ns 786455 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 789764 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.3s 789779 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jmod.dl.proof 789795 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.01ms 789904 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_14816186016960375122.key 789904 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_14816186016960375122.key 789904 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 189.1ns 789904 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 793126 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.22s 793141 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl_14816186016960375122.key 793141 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.4ns 793251 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 793251 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 793251 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 276.3ns 793251 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 796472 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 796487 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqGetOutside.dl.proof 796519 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.27ms 796629 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_16366565415481245300.key 796629 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_16366565415481245300.key 796629 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 296.9ns 796629 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 799755 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 799771 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_singleton.dl_16366565415481245300.key 799787 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.9ns 799896 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_15295378660000206690.key 799896 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_15295378660000206690.key 799896 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 257.6ns 799896 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 803007 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 803023 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_create.dl_15295378660000206690.key 803038 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.8ns 803149 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_8316229932576890085.key 803149 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_8316229932576890085.key 803149 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 216.6ns 803149 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 806213 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 806229 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allFields.dl_8316229932576890085.key 806229 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.5ns 806338 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_5247178512640934349.key 806338 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_5247178512640934349.key 806338 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 427.2ns 806338 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 809371 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 809387 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqEmpty.dl_5247178512640934349.key 809387 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.5ns 809496 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_9812631338754376794.key 809496 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_9812631338754376794.key 809496 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 353ns 809496 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 812560 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 812576 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_union.dl_9812631338754376794.key 812576 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.7ns 812686 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_15184022523977918561.key 812686 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_15184022523977918561.key 812686 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 489.9ns 812686 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 815625 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.94s 815641 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl.2_15184022523977918561.key 815656 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.3ns 815766 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_13784405547082206674.key 815766 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_13784405547082206674.key 815766 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 341.3ns 815766 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 818720 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s 818736 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_wellFormed.dl_13784405547082206674.key 818736 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.3ns 818845 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 818845 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 818845 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 165.4ns 818845 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 821878 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 821941 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jdiv.dl.proof 821941 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.63ms 822066 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_15649400568435592446.key 822066 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_15649400568435592446.key 822066 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 364.6ns 822066 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 825069 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 825085 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_empty.dl_15649400568435592446.key 825085 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.4ns 825194 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_9337316012524267117.key 825194 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_9337316012524267117.key 825194 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 218.4ns 825194 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 828118 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s 828133 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allLocs.dl_9337316012524267117.key 828133 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.6ns 828243 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_14469882134670256942.key 828243 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_14469882134670256942.key 828243 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 306.7ns 828243 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 831275 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 831291 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_arrayRange.dl_14469882134670256942.key 831291 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.1ns 831400 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_5620142717541903271.key 831400 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_5620142717541903271.key 831400 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 267.3ns 831400 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 834402 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 834418 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl_5620142717541903271.key 834434 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.1ns 834544 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_12571749886176468027.key 834544 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_12571749886176468027.key 834544 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 367.8ns 834544 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 837592 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 837608 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqLen.dl_12571749886176468027.key 837608 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.3ns 837718 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_1221193017135939099.key 837718 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_1221193017135939099.key 837718 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 239.7ns 837718 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 840954 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.23s 840970 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_length.dl_1221193017135939099.key 840970 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.8ns 841079 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_17968834334832187907.key 841079 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_17968834334832187907.key 841079 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 264.4ns 841079 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 844393 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.31s 844409 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_freshLocs.dl_17968834334832187907.key 844409 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.3ns 844518 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_3428215570425133535.key 844518 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_3428215570425133535.key 844518 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 246.7ns 844518 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 847661 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 847693 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_anon.dl_3428215570425133535.key 847693 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.1ns 847802 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_18403456440903869122.key 847802 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_18403456440903869122.key 847802 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 345.2ns 847802 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 850991 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 851007 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_memset.dl_18403456440903869122.key 851007 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.4ns 851132 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_10535355282339300172.key 851132 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_10535355282339300172.key 851132 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 217.3ns 851132 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 854306 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 854321 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_store.dl_10535355282339300172.key 854321 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.5ns 854431 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_12798949672894533040.key 854431 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_12798949672894533040.key 854431 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 386.4ns 854431 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 857636 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 857652 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl.2_12798949672894533040.key 857652 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.4ns 857762 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_12854116199751608705.key 857762 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_12854116199751608705.key 857762 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 195.8ns 857762 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 860888 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 860920 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl_12854116199751608705.key 860920 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12ns 861029 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_15050712481261231473.key 861029 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_15050712481261231473.key 861029 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.27ms 861029 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 864202 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 864234 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl.2_15050712481261231473.key 864234 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.8ns 864343 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_38034547839183148.key 864343 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_38034547839183148.key 864343 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 350.4ns 864343 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 867518 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 867534 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_null.dl_38034547839183148.key 867534 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.4ns