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.642s | 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.711s | passed |
| [12] empty.dl, \forall Object o; \forall Field f; ( elementOf(o,f,empty)<<Trigger>> <-> false ) | testSMTLemmaSoundness(String, String)[12] | 2.614s | passed |
| [13] allLocs.dl, \forall Object o; \forall Field f; ( elementOf(o,f,allLocs)<<Trigger>> <-> true ) | testSMTLemmaSoundness(String, String)[13] | 2.618s | 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.660s | 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.644s | passed |
| [16] seqLen.dl, \forall Seq s; seqLen(s)<<Trigger>> >= 0 | testSMTLemmaSoundness(String, String)[16] | 2.658s | passed |
| [17] length.dl, \forall Object o; length(o) >= 0 | testSMTLemmaSoundness(String, String)[17] | 2.629s | 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.606s | 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.647s | passed |
| [1] jmod.dl, \forall int divNum; \forall int divDenom; jmod(divNum,divDenom) = divNum + jdiv(divNum,divDenom)*(-1)*divDenom | testSMTLemmaSoundness(String, String)[1] | 2.719s | 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.632s | 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.651s | 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.674s | passed |
| [23] seqSingleton.dl, \forall any x; any::seqGet(seqSingleton(x)<<Trigger>>, 0) = x | testSMTLemmaSoundness(String, String)[23] | 2.616s | passed |
| [24] seqSingleton.dl.2, \forall any x; seqLen(seqSingleton(x)<<Trigger>>) = 1 | testSMTLemmaSoundness(String, String)[24] | 2.628s | passed |
| [25] null.dl, \forall any x; ((Null::instance(x))<<Trigger>> = TRUE -> x = null) | testSMTLemmaSoundness(String, String)[25] | 2.624s | 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.807s | 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.726s | 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.683s | 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.708s | 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.647s | passed |
| [7] seqEmpty.dl, seqLen(seqEmpty) = 0 | testSMTLemmaSoundness(String, String)[7] | 2.626s | 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.655s | 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.627s | passed |
Standard output
620736 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 620736 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 620736 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.7ns 620736 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 623324 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.59s 623340 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jmod.dl.proof 623340 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.31ms 623455 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_6008782815956519179.key 623455 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_6008782815956519179.key 623455 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 179.4ns 623455 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 626121 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.67s 626136 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl_6008782815956519179.key 626136 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.6ns 626248 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 626248 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 626248 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 359.1ns 626263 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 628826 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.57s 628842 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqGetOutside.dl.proof 628857 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.33ms 628974 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_11427138709951176963.key 628974 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_11427138709951176963.key 628974 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 185.7ns 628974 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 631526 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 631541 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_singleton.dl_11427138709951176963.key 631541 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.9ns 631657 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_8475634259883225965.key 631657 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_8475634259883225965.key 631657 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 273.7ns 631657 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 634240 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.59s 634256 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_create.dl_8475634259883225965.key 634256 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.5ns 634365 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_3596989566804044174.key 634365 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_3596989566804044174.key 634365 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 257.9ns 634365 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 636888 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 636903 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allFields.dl_3596989566804044174.key 636903 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.2ns 637013 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_1400837684086073782.key 637013 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_1400837684086073782.key 637013 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 285.7ns 637013 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 639514 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 639530 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqEmpty.dl_1400837684086073782.key 639530 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.7ns 639640 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_10309934258519172427.key 639640 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_10309934258519172427.key 639640 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 181.3ns 639640 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 642169 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 642185 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_union.dl_10309934258519172427.key 642185 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.4ns 642295 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_9327897344682895317.key 642295 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_9327897344682895317.key 642295 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 193ns 642295 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 644796 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 644812 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl.2_9327897344682895317.key 644812 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.9ns 644921 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_6367928211644483224.key 644921 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_6367928211644483224.key 644921 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 262.6ns 644921 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 647439 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 647455 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_wellFormed.dl_6367928211644483224.key 647455 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.1ns 647564 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 647564 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 647564 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 129.3ns 647564 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 650144 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.59s 650160 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jdiv.dl.proof 650160 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.46ms 650275 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_519829558842230412.key 650275 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_519829558842230412.key 650275 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 274.1ns 650275 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 652761 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 652777 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_empty.dl_519829558842230412.key 652777 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.8ns 652889 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_15618399888699605889.key 652889 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_15618399888699605889.key 652889 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 178.8ns 652889 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 655377 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 655393 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allLocs.dl_15618399888699605889.key 655393 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.4ns 655508 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_6483604501539550992.key 655508 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_6483604501539550992.key 655508 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 250.4ns 655508 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 658042 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 658058 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_arrayRange.dl_6483604501539550992.key 658058 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.2ns 658167 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_14363185618184350897.key 658167 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_14363185618184350897.key 658167 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 179.8ns 658167 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 660687 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 660703 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl_14363185618184350897.key 660703 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.1ns 660812 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_15254106783757366774.key 660812 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_15254106783757366774.key 660812 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 172.1ns 660812 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 663340 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 663356 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqLen.dl_15254106783757366774.key 663356 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.8ns 663470 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_5988765426942091449.key 663470 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_5988765426942091449.key 663470 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 201.6ns 663470 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 665984 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 665984 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_length.dl_5988765426942091449.key 665984 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8ns 666100 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_18209428119488714538.key 666100 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_18209428119488714538.key 666100 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 179.1ns 666100 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 668591 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 668591 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_freshLocs.dl_18209428119488714538.key 668591 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.2ns 668706 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_1092923723105795099.key 668706 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_1092923723105795099.key 668706 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 187.8ns 668706 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 671228 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 671244 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_anon.dl_1092923723105795099.key 671244 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.9ns 671353 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_3271448155297346731.key 671353 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_3271448155297346731.key 671353 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 202.5ns 671353 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 673858 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 673874 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_memset.dl_3271448155297346731.key 673874 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.1ns 673985 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_4173901150083682009.key 673985 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_4173901150083682009.key 673985 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 181.2ns 673985 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 676512 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 676527 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_store.dl_4173901150083682009.key 676527 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8ns 676637 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_18200787640359772392.key 676637 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_18200787640359772392.key 676637 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 263.5ns 676637 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 679186 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 679201 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl.2_18200787640359772392.key 679201 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.9ns 679311 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_6579501085832389470.key 679311 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_6579501085832389470.key 679311 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 206.7ns 679311 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 681802 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 681817 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl_6579501085832389470.key 681817 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.4ns 681927 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_16608189121517627193.key 681927 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_16608189121517627193.key 681927 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 255ns 681927 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 684440 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 684440 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl.2_16608189121517627193.key 684440 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.9ns 684556 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_17162953370295214808.key 684556 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_17162953370295214808.key 684556 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 193.4ns 684556 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 687055 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 687071 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_null.dl_17162953370295214808.key 687071 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7ns