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.329s | 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.252s | passed |
| [12] empty.dl, \forall Object o; \forall Field f; ( elementOf(o,f,empty)<<Trigger>> <-> false ) | testSMTLemmaSoundness(String, String)[12] | 3.377s | passed |
| [13] allLocs.dl, \forall Object o; \forall Field f; ( elementOf(o,f,allLocs)<<Trigger>> <-> true ) | testSMTLemmaSoundness(String, String)[13] | 3.190s | 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.252s | 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.095s | passed |
| [16] seqLen.dl, \forall Seq s; seqLen(s)<<Trigger>> >= 0 | testSMTLemmaSoundness(String, String)[16] | 3.121s | passed |
| [17] length.dl, \forall Object o; length(o) >= 0 | testSMTLemmaSoundness(String, String)[17] | 3.143s | 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.190s | 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.147s | passed |
| [1] jmod.dl, \forall int divNum; \forall int divDenom; jmod(divNum,divDenom) = divNum + jdiv(divNum,divDenom)*(-1)*divDenom | testSMTLemmaSoundness(String, String)[1] | 3.367s | 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.205s | 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.158s | 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.220s | passed |
| [23] seqSingleton.dl, \forall any x; any::seqGet(seqSingleton(x)<<Trigger>>, 0) = x | testSMTLemmaSoundness(String, String)[23] | 3.204s | passed |
| [24] seqSingleton.dl.2, \forall any x; seqLen(seqSingleton(x)<<Trigger>>) = 1 | testSMTLemmaSoundness(String, String)[24] | 3.431s | passed |
| [25] null.dl, \forall any x; ((Null::instance(x))<<Trigger>> = TRUE -> x = null) | testSMTLemmaSoundness(String, String)[25] | 3.394s | 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.267s | 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.379s | 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.189s | 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.409s | 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.268s | passed |
| [7] seqEmpty.dl, seqLen(seqEmpty) = 0 | testSMTLemmaSoundness(String, String)[7] | 3.580s | 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.266s | 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.206s | passed |
Standard output
844362 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 844362 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 844362 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 117.1ns 844377 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 847597 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.23s 847612 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jmod.dl.proof 847628 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6ms 847738 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_10563054471831279779.key 847738 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_10563054471831279779.key 847738 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 181.5ns 847738 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 850880 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 850896 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl_10563054471831279779.key 850896 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.3ns 851005 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 851005 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 851005 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 452ns 851005 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 854227 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.22s 854243 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqGetOutside.dl.proof 854274 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.52ms 854384 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_1057878058898866081.key 854384 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_1057878058898866081.key 854384 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 305.4ns 854384 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 857432 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 857448 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_singleton.dl_1057878058898866081.key 857463 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8ns 857573 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_2233765769467330086.key 857573 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_2233765769467330086.key 857573 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 255.7ns 857573 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 860841 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.27s 860857 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_create.dl_2233765769467330086.key 860857 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.7ns 860982 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_9324952724649222278.key 860982 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_9324952724649222278.key 860982 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 223.3ns 860982 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 864125 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 864140 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allFields.dl_9324952724649222278.key 864140 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9ns 864250 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_3371479291534076301.key 864250 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_3371479291534076301.key 864250 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 306.2ns 864250 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 867705 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.45s 867721 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqEmpty.dl_3371479291534076301.key 867721 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.7ns 867830 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_14832039828909134648.key 867830 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_14832039828909134648.key 867830 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 388.6ns 867830 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 870972 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 870988 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_union.dl_14832039828909134648.key 870988 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.2ns 871097 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_14173860860569311646.key 871097 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_14173860860569311646.key 871097 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 222.8ns 871097 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 874178 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 874194 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl.2_14173860860569311646.key 874194 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.5ns 874303 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_1163661622883814381.key 874303 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_1163661622883814381.key 874303 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 347.6ns 874303 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 877508 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 877523 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_wellFormed.dl_1163661622883814381.key 877523 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.9ns 877633 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 877633 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 877633 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 321.1ns 877633 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 880744 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 880775 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jdiv.dl.proof 880775 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.63ms 880885 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_312395310814281070.key 880885 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_312395310814281070.key 880885 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 275.6ns 880885 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 884121 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.24s 884152 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_empty.dl_312395310814281070.key 884152 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.9ns 884262 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_7539654365657355081.key 884262 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_7539654365657355081.key 884262 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 275.9ns 884262 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 887327 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 887342 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allLocs.dl_7539654365657355081.key 887342 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.7ns 887452 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_16662901097064621594.key 887452 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_16662901097064621594.key 887452 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 272.3ns 887452 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 890563 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 890594 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_arrayRange.dl_16662901097064621594.key 890594 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.2ns 890704 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_11823080634366316374.key 890704 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_11823080634366316374.key 890704 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 178.3ns 890704 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 893674 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 893689 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl_11823080634366316374.key 893689 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.6ns 893799 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_3152942395317027153.key 893799 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_3152942395317027153.key 893799 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 321ns 893799 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 896785 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 896801 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqLen.dl_3152942395317027153.key 896801 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.9ns 896926 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_636240424065070876.key 896926 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_636240424065070876.key 896926 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 380.9ns 896926 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 899944 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 899960 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_length.dl_636240424065070876.key 899960 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.1ns 900069 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_4160874601323166673.key 900069 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_4160874601323166673.key 900069 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 279.8ns 900069 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 903134 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 903150 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_freshLocs.dl_4160874601323166673.key 903150 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.6ns 903259 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_840968000251211151.key 903259 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_840968000251211151.key 903259 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 271.3ns 903259 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 906281 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 906297 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_anon.dl_840968000251211151.key 906297 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.3ns 906406 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_17078158329569883457.key 906406 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_17078158329569883457.key 906406 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 439.7ns 906406 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 909471 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 909486 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_memset.dl_17078158329569883457.key 909501 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.6ns 909611 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_9812616541854362421.key 909611 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_9812616541854362421.key 909611 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 382.4ns 909611 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 912643 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 912660 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_store.dl_9812616541854362421.key 912660 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.8ns 912769 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_6974184695109469483.key 912769 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_6974184695109469483.key 912769 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 480ns 912769 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 915864 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 915880 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl.2_6974184695109469483.key 915880 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8ns 915989 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_2418654285411519596.key 915989 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_2418654285411519596.key 915989 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 333.3ns 915989 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 919053 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 919084 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl_2418654285411519596.key 919084 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.1ns 919193 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_512779916366880741.key 919193 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_512779916366880741.key 919193 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 493.5ns 919209 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 922508 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.3s 922524 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl.2_512779916366880741.key 922524 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.8ns 922633 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_4906256097082913895.key 922633 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_4906256097082913895.key 922633 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 333.4ns 922633 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 925902 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.26s 925917 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_null.dl_4906256097082913895.key 925917 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.9ns