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.187s | 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.598s | passed |
| [12] empty.dl, \forall Object o; \forall Field f; ( elementOf(o,f,empty)<<Trigger>> <-> false ) | testSMTLemmaSoundness(String, String)[12] | 3.532s | passed |
| [13] allLocs.dl, \forall Object o; \forall Field f; ( elementOf(o,f,allLocs)<<Trigger>> <-> true ) | testSMTLemmaSoundness(String, String)[13] | 3.386s | 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.331s | 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.317s | passed |
| [16] seqLen.dl, \forall Seq s; seqLen(s)<<Trigger>> >= 0 | testSMTLemmaSoundness(String, String)[16] | 3.270s | passed |
| [17] length.dl, \forall Object o; length(o) >= 0 | testSMTLemmaSoundness(String, String)[17] | 3.345s | 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.598s | 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.695s | passed |
| [1] jmod.dl, \forall int divNum; \forall int divDenom; jmod(divNum,divDenom) = divNum + jdiv(divNum,divDenom)*(-1)*divDenom | testSMTLemmaSoundness(String, String)[1] | 3.561s | 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.507s | 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.290s | 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.303s | passed |
| [23] seqSingleton.dl, \forall any x; any::seqGet(seqSingleton(x)<<Trigger>>, 0) = x | testSMTLemmaSoundness(String, String)[23] | 3.332s | passed |
| [24] seqSingleton.dl.2, \forall any x; seqLen(seqSingleton(x)<<Trigger>>) = 1 | testSMTLemmaSoundness(String, String)[24] | 3.475s | passed |
| [25] null.dl, \forall any x; ((Null::instance(x))<<Trigger>> = TRUE -> x = null) | testSMTLemmaSoundness(String, String)[25] | 3.577s | 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.252s | 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.238s | 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.311s | 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.380s | 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.488s | passed |
| [7] seqEmpty.dl, seqLen(seqEmpty) = 0 | testSMTLemmaSoundness(String, String)[7] | 3.252s | 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.412s | 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.299s | passed |
Standard output
837624 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 837624 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 837624 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.3ns 837624 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 841063 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.43s 841063 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jmod.dl.proof 841078 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.38ms 841189 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_15615723378423545438.key 841189 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_15615723378423545438.key 841189 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 159ns 841189 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 844316 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 844331 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl_15615723378423545438.key 844331 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.3ns 844441 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 844441 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 844441 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 255.1ns 844441 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 847521 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 847536 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqGetOutside.dl.proof 847568 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 29.79ms 847679 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_17502431172788094312.key 847679 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_17502431172788094312.key 847679 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 213.6ns 847679 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 850849 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 850880 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_singleton.dl_17502431172788094312.key 850880 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.6ns 850990 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_18012545478822165250.key 850990 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_18012545478822165250.key 850990 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 303ns 850990 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 854229 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.24s 854245 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_create.dl_18012545478822165250.key 854245 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.8ns 854370 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_15817776528236607178.key 854370 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_15817776528236607178.key 854370 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 379.1ns 854370 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 857670 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.3s 857701 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allFields.dl_15817776528236607178.key 857701 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.7ns 857859 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_13605572891115758579.key 857859 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_13605572891115758579.key 857859 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 333.6ns 857859 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 860986 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 861001 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqEmpty.dl_13605572891115758579.key 861001 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.7ns 861111 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_10750100117417802231.key 861111 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_10750100117417802231.key 861111 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 174.4ns 861111 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 864398 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.28s 864414 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_union.dl_10750100117417802231.key 864414 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.4ns 864523 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_834320562804110225.key 864523 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_834320562804110225.key 864523 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 214.1ns 864523 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 867681 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 867697 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl.2_834320562804110225.key 867697 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.2ns 867822 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_15948047077431931439.key 867822 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_15948047077431931439.key 867822 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 233.5ns 867822 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 870880 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 870896 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_wellFormed.dl_15948047077431931439.key 870896 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.6ns 871009 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 871009 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 871009 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 443.3ns 871009 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 874214 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 874229 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jdiv.dl.proof 874495 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 263.46ms 874607 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_2390337852451744117.key 874607 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_2390337852451744117.key 874607 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 368.1ns 874607 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 877999 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.39s 878015 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_empty.dl_2390337852451744117.key 878031 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.8ns 878140 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_10757844608306418351.key 878140 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_10757844608306418351.key 878140 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 461.5ns 878140 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 881402 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.25s 881418 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allLocs.dl_10757844608306418351.key 881418 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.7ns 881527 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_1341012648465233104.key 881527 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_1341012648465233104.key 881527 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 519.2ns 881527 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 884729 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 884745 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_arrayRange.dl_1341012648465233104.key 884745 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.7ns 884859 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_17600544333369094120.key 884859 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_17600544333369094120.key 884859 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 332.7ns 884859 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 888049 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 888065 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl_17600544333369094120.key 888065 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.4ns 888176 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_10117938019595863863.key 888176 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_10117938019595863863.key 888176 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 145.1ns 888176 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 891319 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 891336 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqLen.dl_10117938019595863863.key 891336 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9ns 891447 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_10728078919048887119.key 891447 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_10728078919048887119.key 891447 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 664.8ns 891447 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 894668 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.22s 894684 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_length.dl_10728078919048887119.key 894684 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.9ns 894793 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_163947892329342724.key 894793 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_163947892329342724.key 894793 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 285.6ns 894793 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 898265 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.47s 898282 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_freshLocs.dl_163947892329342724.key 898282 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.4ns 898391 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_8632609412090613880.key 898391 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_8632609412090613880.key 898391 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 323.4ns 898391 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 901963 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.57s 901978 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_anon.dl_8632609412090613880.key 901978 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.2ns 902086 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_15654706413234253337.key 902086 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_15654706413234253337.key 902086 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 240.2ns 902086 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 905468 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.37s 905483 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_memset.dl_15654706413234253337.key 905483 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.6ns 905593 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_4246670171845975738.key 905593 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_4246670171845975738.key 905593 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 234.6ns 905593 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 908752 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 908768 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_store.dl_4246670171845975738.key 908768 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.5ns 908883 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_452003029882105283.key 908883 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_452003029882105283.key 908883 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 291.1ns 908883 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 912056 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 912071 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl.2_452003029882105283.key 912071 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.8ns 912186 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_2408288222854847910.key 912186 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_2408288222854847910.key 912186 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 237.2ns 912186 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 915391 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 915407 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl_2408288222854847910.key 915407 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.3ns 915518 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_1140949130703119469.key 915518 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_1140949130703119469.key 915518 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 193.8ns 915518 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 918865 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.35s 918880 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl.2_1140949130703119469.key 918880 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.8ns 918995 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_18405785766309492142.key 918995 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_18405785766309492142.key 918995 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 339.9ns 918995 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 922442 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.44s 922458 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_null.dl_18405785766309492142.key 922458 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.9ns