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.729s | 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.724s | passed |
| [12] empty.dl, \forall Object o; \forall Field f; ( elementOf(o,f,empty)<<Trigger>> <-> false ) | testSMTLemmaSoundness(String, String)[12] | 2.705s | passed |
| [13] allLocs.dl, \forall Object o; \forall Field f; ( elementOf(o,f,allLocs)<<Trigger>> <-> true ) | testSMTLemmaSoundness(String, String)[13] | 2.715s | 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.724s | passed |
| [16] seqLen.dl, \forall Seq s; seqLen(s)<<Trigger>> >= 0 | testSMTLemmaSoundness(String, String)[16] | 2.720s | passed |
| [17] length.dl, \forall Object o; length(o) >= 0 | testSMTLemmaSoundness(String, String)[17] | 2.707s | 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.739s | 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.712s | passed |
| [1] jmod.dl, \forall int divNum; \forall int divDenom; jmod(divNum,divDenom) = divNum + jdiv(divNum,divDenom)*(-1)*divDenom | testSMTLemmaSoundness(String, String)[1] | 2.837s | 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.741s | 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.724s | 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.744s | passed |
| [24] seqSingleton.dl.2, \forall any x; seqLen(seqSingleton(x)<<Trigger>>) = 1 | testSMTLemmaSoundness(String, String)[24] | 2.746s | passed |
| [25] null.dl, \forall any x; ((Null::instance(x))<<Trigger>> = TRUE -> x = null) | testSMTLemmaSoundness(String, String)[25] | 2.713s | 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.813s | 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.790s | 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.734s | 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.745s | 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.713s | passed |
| [7] seqEmpty.dl, seqLen(seqEmpty) = 0 | testSMTLemmaSoundness(String, String)[7] | 2.702s | 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.702s | 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.703s | passed |
Standard output
636047 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 636047 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 636047 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.3ns 636047 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 638739 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.68s 638739 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jmod.dl.proof 638770 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.16ms 638888 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_2851884619141973759.key 638888 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_2851884619141973759.key 638888 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 309.2ns 638888 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 641565 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.67s 641565 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl_2851884619141973759.key 641565 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.3ns 641690 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 641690 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 641690 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 284.3ns 641690 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 644335 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.64s 644350 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqGetOutside.dl.proof 644366 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.1ms 644481 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_9115848828674301663.key 644481 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_9115848828674301663.key 644481 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 213.6ns 644481 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 647085 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.61s 647101 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_singleton.dl_9115848828674301663.key 647101 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.4ns 647214 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_1781222276091956577.key 647214 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_1781222276091956577.key 647214 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 331.7ns 647214 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 649825 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.62s 649849 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_create.dl_1781222276091956577.key 649849 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.2ns 649959 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_8749820203166518485.key 649959 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_8749820203166518485.key 649959 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 219ns 649959 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 652541 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.59s 652557 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allFields.dl_8749820203166518485.key 652557 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.1ns 652672 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_3287590328414782082.key 652672 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_3287590328414782082.key 652672 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 182ns 652672 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 655249 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.58s 655265 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqEmpty.dl_3287590328414782082.key 655265 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.3ns 655374 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_3078153837327373147.key 655374 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_3078153837327373147.key 655374 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 213.8ns 655374 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 657951 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.58s 657967 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_union.dl_3078153837327373147.key 657967 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.9ns 658076 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_17427439802315441349.key 658076 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_17427439802315441349.key 658076 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 203.5ns 658076 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 660654 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.58s 660670 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl.2_17427439802315441349.key 660670 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.9ns 660780 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_14395544068639177406.key 660780 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_14395544068639177406.key 660780 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 313.2ns 660780 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 663379 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.6s 663394 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_wellFormed.dl_14395544068639177406.key 663394 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.5ns 663508 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 663508 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 663508 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 300.3ns 663508 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 666107 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.6s 666107 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jdiv.dl.proof 666123 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.57ms 666233 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_5816001590507696311.key 666233 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_5816001590507696311.key 666233 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 292.9ns 666233 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 668809 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.58s 668825 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_empty.dl_5816001590507696311.key 668825 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.7ns 668939 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_6932430285879517522.key 668939 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_6932430285879517522.key 668939 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 207.7ns 668939 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 671539 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.59s 671539 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allLocs.dl_6932430285879517522.key 671539 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.9ns 671654 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_11474317525285611239.key 671654 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_11474317525285611239.key 671654 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 224.9ns 671654 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 674234 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.58s 674256 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_arrayRange.dl_11474317525285611239.key 674257 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.2ns 674359 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_9012905134245687257.key 674359 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_9012905134245687257.key 674359 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 291.9ns 674359 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 676954 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.59s 676954 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl_9012905134245687257.key 676970 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.3ns 677083 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_2385088754006644772.key 677083 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_2385088754006644772.key 677083 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 312.9ns 677083 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 679687 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.6s 679687 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqLen.dl_2385088754006644772.key 679687 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.1ns 679804 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_1626079468850897272.key 679804 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_1626079468850897272.key 679804 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 304.4ns 679804 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 682383 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.59s 682399 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_length.dl_1626079468850897272.key 682399 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.8ns 682511 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_12341927593721025735.key 682511 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_12341927593721025735.key 682511 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 325ns 682511 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 685101 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.59s 685139 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_freshLocs.dl_12341927593721025735.key 685140 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.4ns 685251 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_3219209764512207438.key 685251 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_3219209764512207438.key 685251 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 202.2ns 685251 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 687838 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.59s 687853 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_anon.dl_3219209764512207438.key 687853 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.7ns 687964 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_4752548726213730637.key 687964 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_4752548726213730637.key 687964 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 209.4ns 687964 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 690565 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.61s 690580 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_memset.dl_4752548726213730637.key 690580 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.7ns 690705 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_1432067746753801415.key 690705 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_1432067746753801415.key 690705 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 211ns 690705 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 693304 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.6s 693320 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_store.dl_1432067746753801415.key 693320 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.3ns 693429 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_12091940264893540264.key 693429 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_12091940264893540264.key 693429 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 303.4ns 693429 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 696035 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.61s 696051 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl.2_12091940264893540264.key 696051 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.9ns 696165 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_17011659400140541931.key 696165 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_17011659400140541931.key 696165 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 212.7ns 696165 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 698784 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.62s 698784 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl_17011659400140541931.key 698800 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8ns 698910 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_10841847032195988939.key 698910 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_10841847032195988939.key 698910 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 294.7ns 698910 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 701509 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.6s 701541 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl.2_10841847032195988939.key 701541 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.5ns 701656 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_3684309154477136023.key 701656 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_3684309154477136023.key 701656 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 227.3ns 701656 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 704241 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.59s 704256 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_null.dl_3684309154477136023.key 704256 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.4ns