Adding dirk-new to repo

[Benchmarks_CSolver.git] / dirk-new / org-traces / pingpong.log

diff --git a/dirk-new/org-traces/pingpong.log b/dirk-new/org-traces/pingpong.log
new file mode 100644 (file)
index 0000000..54dde59
--- /dev/null
+++ b/dirk-new/org-traces/pingpong.log
@@ -0,0 +1,244 @@
+WARNING: unknown parameter 'timeout'
+Legal parameters are:
+  auto_config (bool) (default: true)
+  debug_ref_count (bool) (default: false)
+  dump_models (bool) (default: false)
+  model (bool) (default: true)
+  model_validate (bool) (default: false)
+  proof (bool) (default: false)
+  rlimit (unsigned int) (default: 4294967295)
+  smtlib2_compliant (bool) (default: false)
+  timeout (unsigned int) (default: 4294967295)
+  trace (bool) (default: false)
+  trace_file_name (string) (default: z3.log)
+  type_check (bool) (default: true)
+  unsat_core (bool) (default: false)
+  well_sorted_check (bool) (default: false)
+
+
+ASSERTSTART
+(and (< O!0 O!1)
+     (< O!1 O!2)
+     (< O!2 O!3)
+     (< O!3 O!4)
+     (< O!4 O!5)
+     (< O!5 O!6)
+     (< O!6 O!7)
+     (< O!7 O!8)
+     (< O!8 O!9)
+     (< O!9 O!10)
+     (< O!10 O!11)
+     (< O!11 O!12)
+     (< O!12 O!13)
+     (< O!13 O!14)
+     (< O!14 O!15)
+     (< O!15 O!16)
+     (< O!16 O!17)
+     (< O!17 O!18)
+     (< O!18 O!19)
+     (< O!19 O!20)
+     (< O!20 O!21)
+     (< O!21 O!22)
+     (< O!22 O!23)
+     (< O!23 O!24)
+     (< O!24 O!25)
+     (< O!25 O!26)
+     (< O!26 O!27)
+     (< O!27 O!28)
+     (< O!28 O!29)
+     (< O!29 O!30)
+     (< O!30 O!31)
+     (< O!31 O!32)
+     (< O!32 O!33)
+     (< O!33 O!34)
+     (< O!34 O!35)
+     (< O!35 O!36)
+     (< O!36 O!37)
+     (< O!37 O!38)
+     (< O!39 O!40)
+     (< O!40 O!41)
+     (< O!41 O!42)
+     (< O!43 O!44)
+     (< O!44 O!45)
+     (< O!45 O!46)
+     (< O!47 O!48)
+     (< O!48 O!49)
+     (< O!49 O!50)
+     (< O!51 O!52)
+     (< O!52 O!53)
+     (< O!53 O!54)
+     (< O!55 O!56)
+     (< O!56 O!57)
+     (< O!57 O!58)
+     (< O!59 O!60)
+     (< O!60 O!61)
+     (< O!61 O!62)
+     (< O!63 O!64)
+     (< O!64 O!65)
+     (< O!65 O!66)
+     (< O!67 O!68)
+     (< O!68 O!69)
+     (< O!69 O!70)
+     (< O!71 O!72)
+     (< O!72 O!73)
+     (< O!73 O!74)
+     (< O!75 O!76)
+     (< O!76 O!77)
+     (< O!77 O!78)
+     (< O!79 O!80)
+     (< O!80 O!81)
+     (< O!81 O!82)
+     (< O!83 O!84)
+     (< O!84 O!85)
+     (< O!85 O!86)
+     (< O!87 O!88)
+     (< O!88 O!89)
+     (< O!89 O!90)
+     (< O!91 O!92)
+     (< O!92 O!93)
+     (< O!93 O!94)
+     true)
+ASSERTEND
+
+
+VARSTART
+(=> S!96 true)
+VAREND
+
+
+VARSTART
+(=> S!95 (and S!96 (< O!40 O!42)))
+VAREND
+
+
+VARSTART
+(=> S!100 (< O!3 O!9))
+VAREND
+
+
+VARSTART
+(=> S!101 (< O!5 O!8))
+VAREND
+
+
+VARSTART
+(=> S!102 (< O!1 O!7))
+VAREND
+
+
+VARSTART
+(=> S!103 (< O!0 O!6))
+VAREND
+
+
+VARSTART
+(=> S!99 (and S!100 S!101 S!102 S!103))
+VAREND
+
+
+VARSTART
+(=> S!98 S!99)
+VAREND
+
+
+VARSTART
+(=> S!97 S!98)
+VAREND
+
+
+VARSTART
+(=> S!107 (< O!3 O!11))
+VAREND
+
+
+VARSTART
+(=> S!106 (and S!107 S!100 S!101 S!102 S!103))
+VAREND
+
+
+VARSTART
+(=> S!105 S!106)
+VAREND
+
+
+VARSTART
+(=> S!104 S!105)
+VAREND
+
+
+SATSTART
+(and (= O!42 O!44) S!95 S!97 true S!104 true)
+SATEND
+
+
+TIMESTART
+2019-10-09 21:30:15.579431 UTC
+TIMESTART
+
+
+TIMEEND
+2019-10-09 21:30:15.5798 UTC
+TIMEEND
+
+Found: pingpong/BuggedProgram.pingPong:()V!1 pingpong/BuggedProgram.pingPong:()V!15
+    -:    37 | t1.0009 write r!3.pingPongPlayer r!0
+    -:   143 | t2.0005 read r!3.pingPongPlayer r!0
+
+VARSTART
+(=> S!111 (< O!3 O!13))
+VAREND
+
+
+VARSTART
+(=> S!110 (and S!111 S!107 S!100 S!101 S!102 S!103))
+VAREND
+
+
+VARSTART
+(=> S!109 S!110)
+VAREND
+
+
+VARSTART
+(=> S!108 S!109)
+VAREND
+
+
+SATSTART
+(and (= O!46 O!49) S!104 true S!108 true)
+SATEND
+
+
+TIMESTART
+2019-10-09 21:30:15.581071 UTC
+TIMESTART
+
+
+TIMEEND
+2019-10-09 21:30:15.581303 UTC
+TIMEEND
+
+Found: pingpong/BuggedProgram.pingPong:()V!48 pingpong/BuggedProgram.pingPong:()V!53
+    -:   185 | t2.0007 write r!3.bugAppearanceNumber i32!1
+    -:   430 | t3.0006 read r!3.bugAppearanceNumber i32!1
+
+SATSTART
+(and (= O!46 O!50) S!104 true S!108 true)
+SATEND
+
+
+TIMESTART
+2019-10-09 21:30:15.594731 UTC
+TIMESTART
+
+
+TIMEEND
+2019-10-09 21:30:15.594966 UTC
+TIMEEND
+
+Found: pingpong/BuggedProgram.pingPong:()V!53 pingpong/BuggedProgram.pingPong:()V!53
+    -:   185 | t2.0007 write r!3.bugAppearanceNumber i32!1
+    -:   443 | t3.0007 write r!3.bugAppearanceNumber i32!2
+pingpong/BuggedProgram.pingPong:()V!1 pingpong/BuggedProgram.pingPong:()V!15
+pingpong/BuggedProgram.pingPong:()V!48 pingpong/BuggedProgram.pingPong:()V!53
+pingpong/BuggedProgram.pingPong:()V!53 pingpong/BuggedProgram.pingPong:()V!53