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.332s | 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.211s | passed |
| [12] empty.dl, \forall Object o; \forall Field f; ( elementOf(o,f,empty)<<Trigger>> <-> false ) | testSMTLemmaSoundness(String, String)[12] | 3.182s | passed |
| [13] allLocs.dl, \forall Object o; \forall Field f; ( elementOf(o,f,allLocs)<<Trigger>> <-> true ) | testSMTLemmaSoundness(String, String)[13] | 3.168s | 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.281s | 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.219s | passed |
| [16] seqLen.dl, \forall Seq s; seqLen(s)<<Trigger>> >= 0 | testSMTLemmaSoundness(String, String)[16] | 3.345s | passed |
| [17] length.dl, \forall Object o; length(o) >= 0 | testSMTLemmaSoundness(String, String)[17] | 3.134s | 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.204s | 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.182s | passed |
| [1] jmod.dl, \forall int divNum; \forall int divDenom; jmod(divNum,divDenom) = divNum + jdiv(divNum,divDenom)*(-1)*divDenom | testSMTLemmaSoundness(String, String)[1] | 3.271s | 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.270s | 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.297s | 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.270s | passed |
| [23] seqSingleton.dl, \forall any x; any::seqGet(seqSingleton(x)<<Trigger>>, 0) = x | testSMTLemmaSoundness(String, String)[23] | 3.237s | passed |
| [24] seqSingleton.dl.2, \forall any x; seqLen(seqSingleton(x)<<Trigger>>) = 1 | testSMTLemmaSoundness(String, String)[24] | 3.226s | passed |
| [25] null.dl, \forall any x; ((Null::instance(x))<<Trigger>> = TRUE -> x = null) | testSMTLemmaSoundness(String, String)[25] | 3.207s | 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.295s | 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.408s | 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.406s | 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.259s | 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.174s | passed |
| [7] seqEmpty.dl, seqLen(seqEmpty) = 0 | testSMTLemmaSoundness(String, String)[7] | 3.245s | 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.236s | 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.211s | passed |
Standard output
760561 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 760561 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 760561 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.5ns 760561 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 763688 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 763720 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jmod.dl.proof 763720 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.45ms 763829 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_17875049015922645655.key 763829 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_17875049015922645655.key 763829 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 155.4ns 763829 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 766993 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 767008 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl_17875049015922645655.key 767008 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.2ns 767124 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 767124 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 767124 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.5ns 767140 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 770376 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.25s 770392 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqGetOutside.dl.proof 770423 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.27ms 770532 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_8377555694829626813.key 770532 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_8377555694829626813.key 770532 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 264.3ns 770532 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 773807 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.28s 773822 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_singleton.dl_8377555694829626813.key 773822 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.2ns 773938 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_7704104187359096930.key 773938 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_7704104187359096930.key 773938 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 140.8ns 773938 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 777072 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 777088 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_create.dl_7704104187359096930.key 777088 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9ns 777197 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_10791753503962630831.key 777197 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_10791753503962630831.key 777197 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 158.6ns 777197 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 780246 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 780261 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allFields.dl_10791753503962630831.key 780261 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.1ns 780371 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_8827641450238978711.key 780371 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_8827641450238978711.key 780371 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 144.5ns 780371 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 783475 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 783491 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqEmpty.dl_8827641450238978711.key 783506 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.1ns 783616 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_3378249425708245093.key 783616 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_3378249425708245093.key 783616 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 133.4ns 783616 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 786712 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 786727 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_union.dl_3378249425708245093.key 786743 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.9ns 786852 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_7734087879187479278.key 786852 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_7734087879187479278.key 786852 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 142.5ns 786852 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 789938 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 789953 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl.2_7734087879187479278.key 789953 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9ns 790063 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_6220021180020010243.key 790063 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_6220021180020010243.key 790063 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 284.2ns 790063 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 793255 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 793286 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_wellFormed.dl_6220021180020010243.key 793286 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.1ns 793395 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 793395 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 793395 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 99.5ns 793395 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 796465 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 796481 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jdiv.dl.proof 796497 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.02ms 796606 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_8368872068403003118.key 796606 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_8368872068403003118.key 796606 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 156.6ns 796606 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 799656 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 799672 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_empty.dl_8368872068403003118.key 799672 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.4ns 799789 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_5147185650686408941.key 799789 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_5147185650686408941.key 799789 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 258.7ns 799789 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 802827 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 802842 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allLocs.dl_5147185650686408941.key 802842 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.3ns 802957 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_16804703312884710095.key 802957 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_16804703312884710095.key 802957 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 246ns 802957 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 806067 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 806130 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_arrayRange.dl_16804703312884710095.key 806130 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9ns 806238 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_12092527162113229371.key 806238 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_12092527162113229371.key 806238 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 135.1ns 806238 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 809318 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 809333 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl_12092527162113229371.key 809333 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.3ns 809458 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_8836193165532383840.key 809458 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_8836193165532383840.key 809458 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 244.2ns 809458 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 812679 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 812695 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqLen.dl_8836193165532383840.key 812695 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.5ns 812804 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_5089763666022411206.key 812804 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_5089763666022411206.key 812804 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 270.1ns 812804 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 815813 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 815829 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_length.dl_5089763666022411206.key 815829 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.3ns 815938 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_6668054117464605571.key 815938 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_6668054117464605571.key 815938 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 248.6ns 815938 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 819017 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 819033 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_freshLocs.dl_6668054117464605571.key 819033 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.3ns 819142 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_2778106961329366406.key 819142 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_2778106961329366406.key 819142 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 150.5ns 819142 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 822199 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 822214 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_anon.dl_2778106961329366406.key 822214 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.4ns 822324 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_11076516744344191134.key 822324 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_11076516744344191134.key 822324 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 153.5ns 822324 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 825436 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 825484 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_memset.dl_11076516744344191134.key 825484 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.3ns 825594 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_7306939203838995974.key 825594 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_7306939203838995974.key 825594 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 349.4ns 825594 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 828760 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 828776 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_store.dl_7306939203838995974.key 828776 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.8ns 828893 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_7506174021599835577.key 828893 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_7506174021599835577.key 828893 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 349.2ns 828893 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 832038 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 832054 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl.2_7506174021599835577.key 832054 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.9ns 832163 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_7335891229891836276.key 832163 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_7335891229891836276.key 832163 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 254.5ns 832163 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 835275 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 835290 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl_7335891229891836276.key 835290 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10ns 835400 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_6037486844407312472.key 835400 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_6037486844407312472.key 835400 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 132ns 835400 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 838501 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 838517 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl.2_6037486844407312472.key 838517 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.8ns 838628 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_17218536236946101683.key 838628 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_17218536236946101683.key 838628 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 548.9ns 838628 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 841708 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 841724 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_null.dl_17218536236946101683.key 841724 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.4ns