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.767s | 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.688s | passed |
| [12] empty.dl, \forall Object o; \forall Field f; ( elementOf(o,f,empty)<<Trigger>> <-> false ) | testSMTLemmaSoundness(String, String)[12] | 2.813s | passed |
| [13] allLocs.dl, \forall Object o; \forall Field f; ( elementOf(o,f,allLocs)<<Trigger>> <-> true ) | testSMTLemmaSoundness(String, String)[13] | 2.704s | 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.751s | 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.689s | passed |
| [16] seqLen.dl, \forall Seq s; seqLen(s)<<Trigger>> >= 0 | testSMTLemmaSoundness(String, String)[16] | 2.704s | 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.707s | 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.735s | 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.720s | 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.766s | 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.704s | passed |
| [23] seqSingleton.dl, \forall any x; any::seqGet(seqSingleton(x)<<Trigger>>, 0) = x | testSMTLemmaSoundness(String, String)[23] | 2.749s | 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.765s | 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.759s | 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.891s | 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.751s | 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.829s | 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.752s | passed |
| [7] seqEmpty.dl, seqLen(seqEmpty) = 0 | testSMTLemmaSoundness(String, String)[7] | 2.752s | 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.798s | 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.752s | passed |
Standard output
663337 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 663337 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 663337 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 115.7ns 663337 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 666041 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.7s 666056 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jmod.dl.proof 666072 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.82ms 666181 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_1430293147353628014.key 666181 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_1430293147353628014.key 666181 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 399.9ns 666181 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.63s 668824 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl_1430293147353628014.key 668824 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.8ns 668934 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 668934 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 668934 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 180.5ns 668934 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 671669 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 671685 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqGetOutside.dl.proof 671716 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.18ms 671825 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_6285634670049423402.key 671825 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_6285634670049423402.key 671825 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 336.2ns 671825 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 674452 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.62s 674468 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_singleton.dl_6285634670049423402.key 674468 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.5ns 674577 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_8513991416104656275.key 674577 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_8513991416104656275.key 674577 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 280.6ns 674577 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 677281 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.7s 677297 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_create.dl_8513991416104656275.key 677297 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.8ns 677406 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_10953100205383685384.key 677406 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_10953100205383685384.key 677406 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 164.4ns 677406 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 680033 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.62s 680048 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allFields.dl_10953100205383685384.key 680048 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.3ns 680158 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_6893830847857918080.key 680158 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_6893830847857918080.key 680158 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 226.9ns 680158 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 682786 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.63s 682801 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqEmpty.dl_6893830847857918080.key 682801 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.2ns 682911 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_4015979452025231503.key 682911 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_4015979452025231503.key 682911 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 229.5ns 682911 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 685568 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.67s 685583 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_union.dl_4015979452025231503.key 685599 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.1ns 685709 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_17772709888720063962.key 685709 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_17772709888720063962.key 685709 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 217.6ns 685709 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 688335 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.62s 688351 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl.2_17772709888720063962.key 688351 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.8ns 688461 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_16779990998546732843.key 688461 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_16779990998546732843.key 688461 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 236.9ns 688461 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 691102 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.64s 691118 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_wellFormed.dl_16779990998546732843.key 691118 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.4ns 691228 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 691228 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 691228 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 159.6ns 691228 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 693791 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 693807 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jdiv.dl.proof 693807 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2ms 693916 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_1086357219642542643.key 693916 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_1086357219642542643.key 693916 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 445ns 693916 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 696543 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.63s 696558 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_empty.dl_1086357219642542643.key 696621 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.7ns 696730 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_5295874640919697242.key 696730 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_5295874640919697242.key 696730 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 246.8ns 696730 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 699310 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.57s 699325 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allLocs.dl_5295874640919697242.key 699325 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.7ns 699435 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_7476675622438447746.key 699435 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_7476675622438447746.key 699435 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 225.9ns 699435 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 702061 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.62s 702076 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_arrayRange.dl_7476675622438447746.key 702076 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.7ns 702186 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_9252412129236749001.key 702186 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_9252412129236749001.key 702186 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 236.9ns 702186 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 704750 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.57s 704766 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl_9252412129236749001.key 704766 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.6ns 704875 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_13292498263883662795.key 704875 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_13292498263883662795.key 704875 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 246.9ns 704875 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 707455 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.58s 707471 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqLen.dl_13292498263883662795.key 707471 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5ns 707580 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_6104255138602000904.key 707580 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_6104255138602000904.key 707580 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 242.5ns 707580 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 710190 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.62s 710206 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_length.dl_6104255138602000904.key 710206 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.4ns 710315 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_3285662888067452195.key 710315 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_3285662888067452195.key 710315 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 247.1ns 710315 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 712897 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.58s 712913 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_freshLocs.dl_3285662888067452195.key 712913 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.2ns 713022 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_3133008501247583757.key 713022 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_3133008501247583757.key 713022 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 146.9ns 713022 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 715632 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.61s 715648 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_anon.dl_3133008501247583757.key 715648 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.4ns 715757 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_533062194827679688.key 715757 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_533062194827679688.key 715757 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 353.2ns 715757 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 718352 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.6s 718368 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_memset.dl_533062194827679688.key 718368 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.2ns 718478 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_13289329719144745484.key 718478 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_13289329719144745484.key 718478 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 349.6ns 718478 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 721119 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.64s 721135 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_store.dl_13289329719144745484.key 721135 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.4ns 721244 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_2265825929397785352.key 721244 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_2265825929397785352.key 721244 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 248.8ns 721244 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 723824 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.58s 723839 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl.2_2265825929397785352.key 723839 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.3ns 723949 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_1119207008517885947.key 723949 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_1119207008517885947.key 723949 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 309.6ns 723949 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 726575 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.63s 726591 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl_1119207008517885947.key 726591 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.7ns 726701 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_3577359272548002364.key 726701 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_3577359272548002364.key 726701 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 132.2ns 726701 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 729296 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.6s 729311 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl.2_3577359272548002364.key 729311 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.2ns 729421 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_4142639263930474426.key 729421 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_4142639263930474426.key 729421 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 228.4ns 729421 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 732062 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.64s 732078 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_null.dl_4142639263930474426.key 732078 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.5ns