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.744s | 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.728s | passed |
| [12] empty.dl, \forall Object o; \forall Field f; ( elementOf(o,f,empty)<<Trigger>> <-> false ) | testSMTLemmaSoundness(String, String)[12] | 2.748s | passed |
| [13] allLocs.dl, \forall Object o; \forall Field f; ( elementOf(o,f,allLocs)<<Trigger>> <-> true ) | testSMTLemmaSoundness(String, String)[13] | 2.741s | 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.718s | 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.758s | passed |
| [16] seqLen.dl, \forall Seq s; seqLen(s)<<Trigger>> >= 0 | testSMTLemmaSoundness(String, String)[16] | 2.727s | passed |
| [17] length.dl, \forall Object o; length(o) >= 0 | testSMTLemmaSoundness(String, String)[17] | 2.748s | 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.729s | 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.770s | passed |
| [1] jmod.dl, \forall int divNum; \forall int divDenom; jmod(divNum,divDenom) = divNum + jdiv(divNum,divDenom)*(-1)*divDenom | testSMTLemmaSoundness(String, String)[1] | 2.859s | 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.733s | 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.727s | 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.732s | passed |
| [23] seqSingleton.dl, \forall any x; any::seqGet(seqSingleton(x)<<Trigger>>, 0) = x | testSMTLemmaSoundness(String, String)[23] | 2.709s | passed |
| [24] seqSingleton.dl.2, \forall any x; seqLen(seqSingleton(x)<<Trigger>>) = 1 | testSMTLemmaSoundness(String, String)[24] | 2.764s | passed |
| [25] null.dl, \forall any x; ((Null::instance(x))<<Trigger>> = TRUE -> x = null) | testSMTLemmaSoundness(String, String)[25] | 2.722s | 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.793s | passed |
| [3] seqGetOutside.dl, \forall int i; \forall Seq s; ( i < 0 | i >= seqLen(s) -> any::seqGet(s, i)<<Trigger>> = seqGetOutside ) | testSMTLemmaSoundness(String, String)[3] | 2.856s | 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.782s | 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.801s | 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.751s | passed |
| [7] seqEmpty.dl, seqLen(seqEmpty) = 0 | testSMTLemmaSoundness(String, String)[7] | 2.734s | 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.754s | 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.716s | passed |
Standard output
640835 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 640835 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 640835 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 84ns 640835 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 643563 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 643579 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jmod.dl.proof 643594 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.31ms 643704 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_14139284815935546758.key 643704 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_14139284815935546758.key 643704 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 230.7ns 643704 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 646363 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.66s 646379 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl_14139284815935546758.key 646379 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.8ns 646492 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 646492 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 646492 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 314.8ns 646492 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 649207 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s 649207 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqGetOutside.dl.proof 649238 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.04ms 649348 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_14478723630329406409.key 649348 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_14478723630329406409.key 649348 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 220.8ns 649348 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 652005 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.65s 652021 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_singleton.dl_14478723630329406409.key 652021 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.2ns 652131 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_11984124945664802969.key 652131 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_11984124945664802969.key 652131 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 364.7ns 652131 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 654808 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.67s 654823 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_create.dl_11984124945664802969.key 654823 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.3ns 654932 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_11388530475095508532.key 654932 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_11388530475095508532.key 654932 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 229.5ns 654932 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 657559 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.62s 657559 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allFields.dl_11388530475095508532.key 657574 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.6ns 657684 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_5736645073185423259.key 657684 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_5736645073185423259.key 657684 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 131.8ns 657684 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 660293 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.61s 660309 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqEmpty.dl_5736645073185423259.key 660309 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.9ns 660418 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_10388333212742184648.key 660418 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_10388333212742184648.key 660418 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 232.3ns 660418 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 663047 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.63s 663062 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_union.dl_10388333212742184648.key 663062 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.1ns 663172 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_7442963948420106910.key 663172 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_7442963948420106910.key 663172 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 224.3ns 663172 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 665764 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.59s 665779 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl.2_7442963948420106910.key 665779 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.5ns 665889 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_5666206522788130352.key 665889 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_5666206522788130352.key 665889 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 225.6ns 665889 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 668499 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.62s 668515 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_wellFormed.dl_5666206522788130352.key 668515 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.7ns 668632 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 668632 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 668632 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 271.7ns 668632 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 671221 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.59s 671237 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jdiv.dl.proof 671252 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.71ms 671362 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_3373663196166288187.key 671362 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_3373663196166288187.key 671362 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 308.2ns 671362 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 673983 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.63s 673999 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_empty.dl_3373663196166288187.key 673999 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.3ns 674111 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_11939156286926713421.key 674111 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_11939156286926713421.key 674111 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 320.4ns 674111 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 676728 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.61s 676728 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allLocs.dl_11939156286926713421.key 676743 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.6ns 676852 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_5517651513626348017.key 676852 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_5517651513626348017.key 676852 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 222.9ns 676852 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 679435 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.59s 679451 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_arrayRange.dl_5517651513626348017.key 679451 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.6ns 679571 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_11621577258988078659.key 679571 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_11621577258988078659.key 679571 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 319.7ns 679571 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 682206 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.63s 682221 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl_11621577258988078659.key 682221 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.2ns 682330 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_15151052342408894068.key 682330 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_15151052342408894068.key 682330 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 215.8ns 682330 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 684926 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.6s 684942 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqLen.dl_15151052342408894068.key 684942 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.9ns 685057 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_441896130288212589.key 685057 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_441896130288212589.key 685057 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 223ns 685057 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 687690 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.63s 687690 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_length.dl_441896130288212589.key 687690 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.9ns 687806 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_11081548022949922276.key 687806 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_11081548022949922276.key 687806 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 223ns 687806 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 690410 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.61s 690426 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_freshLocs.dl_11081548022949922276.key 690426 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.2ns 690535 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_5433731585361971218.key 690535 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_5433731585361971218.key 690535 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 229.4ns 690535 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 693149 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.62s 693195 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_anon.dl_5433731585361971218.key 693195 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.6ns 693305 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_3013928728014839853.key 693305 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_3013928728014839853.key 693305 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 360.6ns 693305 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 695914 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.6s 695930 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_memset.dl_3013928728014839853.key 695930 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8ns 696039 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_8028891855158598001.key 696039 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_8028891855158598001.key 696039 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 230.9ns 696039 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 698640 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.6s 698656 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_store.dl_8028891855158598001.key 698656 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.6ns 698767 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_1458245774250657849.key 698767 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_1458245774250657849.key 698767 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 220.9ns 698767 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 701374 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.61s 701390 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl.2_1458245774250657849.key 701390 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.1ns 701499 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_12372272402291894069.key 701499 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_12372272402291894069.key 701499 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 205.9ns 701499 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 704080 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.59s 704096 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl_12372272402291894069.key 704096 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.1ns 704209 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_11150997500064350550.key 704209 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_11150997500064350550.key 704209 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 317ns 704209 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 706843 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.64s 706859 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl.2_11150997500064350550.key 706859 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.1ns 706973 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_14177231880070465271.key 706973 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_14177231880070465271.key 706973 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 202.7ns 706973 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 709571 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.6s 709587 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_null.dl_14177231880070465271.key 709587 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.9ns