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.905s | 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.912s | passed |
| [12] empty.dl, \forall Object o; \forall Field f; ( elementOf(o,f,empty)<<Trigger>> <-> false ) | testSMTLemmaSoundness(String, String)[12] | 2.888s | passed |
| [13] allLocs.dl, \forall Object o; \forall Field f; ( elementOf(o,f,allLocs)<<Trigger>> <-> true ) | testSMTLemmaSoundness(String, String)[13] | 2.882s | 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.873s | 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.891s | passed |
| [16] seqLen.dl, \forall Seq s; seqLen(s)<<Trigger>> >= 0 | testSMTLemmaSoundness(String, String)[16] | 2.891s | passed |
| [17] length.dl, \forall Object o; length(o) >= 0 | testSMTLemmaSoundness(String, String)[17] | 2.896s | 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.922s | 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.871s | passed |
| [1] jmod.dl, \forall int divNum; \forall int divDenom; jmod(divNum,divDenom) = divNum + jdiv(divNum,divDenom)*(-1)*divDenom | testSMTLemmaSoundness(String, String)[1] | 2.965s | 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.887s | 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.909s | 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.965s | passed |
| [23] seqSingleton.dl, \forall any x; any::seqGet(seqSingleton(x)<<Trigger>>, 0) = x | testSMTLemmaSoundness(String, String)[23] | 2.894s | passed |
| [24] seqSingleton.dl.2, \forall any x; seqLen(seqSingleton(x)<<Trigger>>) = 1 | testSMTLemmaSoundness(String, String)[24] | 2.910s | passed |
| [25] null.dl, \forall any x; ((Null::instance(x))<<Trigger>> = TRUE -> x = null) | testSMTLemmaSoundness(String, String)[25] | 2.888s | 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.951s | 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.094s | 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.895s | 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.882s | 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.886s | passed |
| [7] seqEmpty.dl, seqLen(seqEmpty) = 0 | testSMTLemmaSoundness(String, String)[7] | 2.896s | 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.879s | 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.890s | passed |
Standard output
664015 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 664016 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 664016 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.7ns 664019 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 666837 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 666853 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jmod.dl.proof 666853 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.54ms 666968 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_17948415005318690382.key 666968 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_17948415005318690382.key 666968 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 255.7ns 666968 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 669795 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 669810 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl_17948415005318690382.key 669810 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12ns 669919 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 669982 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 670060 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.77ms 670060 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 672853 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 672869 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqGetOutside.dl.proof 672885 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.18ms 673014 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_5663235510152629808.key 673014 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_5663235510152629808.key 673014 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 225.7ns 673014 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 675784 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 675800 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_singleton.dl_5663235510152629808.key 675800 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.1ns 675910 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_6936396966589178394.key 675910 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_6936396966589178394.key 675910 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 374.9ns 675910 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 678652 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 678667 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_create.dl_6936396966589178394.key 678667 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.6ns 678792 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_12763443193983183618.key 678792 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_12763443193983183618.key 678792 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 300.7ns 678792 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 681549 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 681564 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allFields.dl_12763443193983183618.key 681564 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.4ns 681679 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_13602503746119702317.key 681679 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_13602503746119702317.key 681679 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 399.6ns 681679 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 684444 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 684460 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqEmpty.dl_13602503746119702317.key 684460 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10ns 684575 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_18227399547683686387.key 684575 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_18227399547683686387.key 684575 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 196.5ns 684575 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 687324 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 687340 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_union.dl_18227399547683686387.key 687340 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.1ns 687455 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_13126972711719434623.key 687455 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_13126972711719434623.key 687455 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 292.1ns 687455 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 690220 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 690236 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl.2_13126972711719434623.key 690236 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.2ns 690345 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_6855632362654317748.key 690345 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_6855632362654317748.key 690345 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 310.1ns 690345 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 693125 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 693140 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_wellFormed.dl_6855632362654317748.key 693140 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.2ns 693251 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 693251 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 693251 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 309.8ns 693251 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 696037 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 696053 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jdiv.dl.proof 696053 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.93ms 696163 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_17775809126405740522.key 696163 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_17775809126405740522.key 696163 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 351.8ns 696163 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 698926 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 698942 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_empty.dl_17775809126405740522.key 698942 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.6ns 699052 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_7301187142835418915.key 699052 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_7301187142835418915.key 699052 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 233.4ns 699052 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 701809 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 701824 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allLocs.dl_7301187142835418915.key 701824 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11ns 701934 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_10248674395263780274.key 701934 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_10248674395263780274.key 701934 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 305.5ns 701934 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 704676 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 704692 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_arrayRange.dl_10248674395263780274.key 704692 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10ns 704808 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_17307463994888901979.key 704808 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_17307463994888901979.key 704808 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 233ns 704808 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 707575 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 707575 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl_17307463994888901979.key 707590 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10ns 707699 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_16878833064025561619.key 707699 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_16878833064025561619.key 707699 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 363.2ns 707699 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 710459 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 710474 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqLen.dl_16878833064025561619.key 710474 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.6ns 710591 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_9594636088514529276.key 710591 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_9594636088514529276.key 710591 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 213.6ns 710591 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 713361 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 713377 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_length.dl_9594636088514529276.key 713377 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.4ns 713487 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_6854621132962399457.key 713487 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_6854621132962399457.key 713487 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 263.4ns 713487 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 716247 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 716297 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_freshLocs.dl_6854621132962399457.key 716298 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.8ns 716410 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_15927110471449240465.key 716410 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_15927110471449240465.key 716410 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 230.4ns 716410 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 719152 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 719168 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_anon.dl_15927110471449240465.key 719168 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.7ns 719281 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_3186153442337606341.key 719281 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_3186153442337606341.key 719281 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 363.7ns 719281 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 722044 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 722059 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_memset.dl_3186153442337606341.key 722059 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12ns 722169 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_1051401988437925560.key 722169 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_1051401988437925560.key 722169 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 307.6ns 722169 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 724948 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 724963 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_store.dl_1051401988437925560.key 724963 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.1ns 725079 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_9545917540970049944.key 725079 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_9545917540970049944.key 725079 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 133.8ns 725079 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 727913 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 727928 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl.2_9545917540970049944.key 727928 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.6ns 728045 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_3188940361737186139.key 728045 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_3188940361737186139.key 728045 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 378.6ns 728045 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 730807 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 730823 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl_3188940361737186139.key 730823 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.5ns 730939 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_15786518874430591176.key 730939 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_15786518874430591176.key 730939 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 357.3ns 730939 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 733726 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 733741 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl.2_15786518874430591176.key 733741 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.5ns 733851 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_7329706905087304559.key 733851 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_7329706905087304559.key 733851 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 286.1ns 733851 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 736607 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 736623 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_null.dl_7329706905087304559.key 736623 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14ns