NAME: dotProduct1.c
CITE: \cite{LLNL:OpenMP:URL}
TYPE: $\text{O}$
SCALE: \texttt{NT=3,N=8}

files,language,blank,comment,code,"http://cloc.sourceforge.net v 1.62  T=0.01 s (183.6 files/s, 7528.5 lines/s)"
1,C,5,18,18
civl verify -ompLoopDecomp=ALL -inputTHREAD_MAX=3 -enablePrintf=false  dotProduct1.c
CIVL v0.16 of 2015-1-6 -- http://vsl.cis.udel.edu/civl

=================== Stats ===================
   validCalls          : 85
   proverCalls         : 3
   memory (bytes)      : 650117120
   time (s)            : 1.81
   maxProcs            : 1
   statesInstantiated  : 411
   statesSaved         : 76
   statesSeen          : 75
   statesMatched       : 0
   steps               : 121
   transitions         : 74

The standard properties hold for all executions.
NAME: dotProduct{\U}critical.c
CITE: \cite{PP2012:OpenMP:URL}
TYPE: $\text{O}$
SCALE: \texttt{NT=3,N=100}

files,language,blank,comment,code,"http://cloc.sourceforge.net v 1.62  T=0.01 s (78.1 files/s, 4063.7 lines/s)"
1,C,12,11,29
civl verify -ompLoopDecomp=ALL -inputTHREAD_MAX=3 -enablePrintf=false  dotProduct_critical.c
CIVL v0.16 of 2015-1-6 -- http://vsl.cis.udel.edu/civl
17s: mem=1344Mb steps=42770 trans=37852 seen=37849 saved=37905 prove=10

=================== Stats ===================
   validCalls          : 189525
   proverCalls         : 10
   memory (bytes)      : 1344798720
   time (s)            : 26.41
   maxProcs            : 4
   statesInstantiated  : 595472
   statesSaved         : 63003
   statesSeen          : 62948
   statesMatched       : 23
   steps               : 72020
   transitions         : 62970

The standard properties hold for all executions.
NAME: matProduct1.c
CITE: \cite{LLNL:OpenMP:URL}
TYPE: $\text{O}$
SCALE: \texttt{NT=3,NRA=8,NCA=8,NCB=8}

files,language,blank,comment,code,"http://cloc.sourceforge.net v 1.62  T=0.01 s (74.7 files/s, 6052.9 lines/s)"
1,C,7,19,55
civl verify -ompLoopDecomp=ALL -inputTHREAD_MAX=3 -enablePrintf=false  matProduct1.c
CIVL v0.16 of 2015-1-6 -- http://vsl.cis.udel.edu/civl

=================== Stats ===================
   validCalls          : 5188
   proverCalls         : 3
   memory (bytes)      : 650117120
   time (s)            : 2.18
   maxProcs            : 1
   statesInstantiated  : 9388
   statesSaved         : 1798
   statesSeen          : 1797
   statesMatched       : 0
   steps               : 2886
   transitions         : 1796

The standard properties hold for all executions.
NAME: heated{\U}plate{\U}openmp.c
CITE: \cite{Quinn:Book04}
TYPE: $\text{O}$
SCALE: \texttt{NT=3,M=5,N=5,EPSILON=0.1}

files,language,blank,comment,code,"http://cloc.sourceforge.net v 1.62  T=0.01 s (67.1 files/s, 20122.0 lines/s)"
1,C,44,106,150
civl verify -ompLoopDecomp=ALL -inputTHREAD_MAX=3 -enablePrintf=false  -DMATH_ELABORATE_ASSUMPTIONS heated_plate_openmp.c
CIVL v0.16 of 2015-1-6 -- http://vsl.cis.udel.edu/civl
18s: mem=1307Mb steps=78249 trans=63882 seen=63544 saved=63822 prove=12

=================== Stats ===================
   validCalls          : 289198
   proverCalls         : 12
   memory (bytes)      : 1398276096
   time (s)            : 23.28
   maxProcs            : 4
   statesInstantiated  : 801082
   statesSaved         : 87271
   statesSeen          : 86910
   statesMatched       : 440
   steps               : 107425
   transitions         : 87349

The standard properties hold for all executions.
NAME: fig3.10-mxv-omp.c
CITE: \cite{chapman-etal:2008:using-openmp}
TYPE: $\text{O}$
SCALE: \texttt{NT=3,M=10,N=10}

files,language,blank,comment,code,"http://cloc.sourceforge.net v 1.62  T=0.01 s (67.1 files/s, 6647.5 lines/s)"
1,C,20,36,43
civl verify -ompLoopDecomp=ALL -inputTHREAD_MAX=3 -enablePrintf=false  fig310-mxv-omp.c
CIVL v0.16 of 2015-1-6 -- http://vsl.cis.udel.edu/civl

=================== Stats ===================
   validCalls          : 2521
   proverCalls         : 5
   memory (bytes)      : 650117120
   time (s)            : 2.14
   maxProcs            : 1
   statesInstantiated  : 3605
   statesSaved         : 515
   statesSeen          : 511
   statesMatched       : 0
   steps               : 786
   transitions         : 510

The standard properties hold for all executions.
NAME: quad{\U}openmp.c
CITE: \cite{Burkardt:OpenMP:URL}
TYPE: $\text{O}$
SCALE: \texttt{NT=3,N=100}

files,language,blank,comment,code,"http://cloc.sourceforge.net v 1.62  T=0.02 s (62.8 files/s, 13131.5 lines/s)"
1,C,67,60,82
civl verify -ompLoopDecomp=ALL -inputTHREAD_MAX=3 -enablePrintf=false  quad_openmp.c
CIVL v0.16 of 2015-1-6 -- http://vsl.cis.udel.edu/civl

=================== Stats ===================
   validCalls          : 436
   proverCalls         : 5
   memory (bytes)      : 921698304
   time (s)            : 3.0
   maxProcs            : 1
   statesInstantiated  : 3216
   statesSaved         : 261
   statesSeen          : 259
   statesMatched       : 0
   steps               : 920
   transitions         : 258

The standard properties hold for all executions.
NAME: pi.c
CITE: \cite{PP2012:OpenMP:URL}
TYPE: $\text{O}$
SCALE: \texttt{NT=3,N=100}

files,language,blank,comment,code,"http://cloc.sourceforge.net v 1.62  T=0.01 s (69.6 files/s, 6127.3 lines/s)"
1,C,14,31,43
civl verify -ompLoopDecomp=ALL -inputTHREAD_MAX=3 -enablePrintf=false  pi.c
CIVL v0.16 of 2015-1-6 -- http://vsl.cis.udel.edu/civl

=================== Stats ===================
   validCalls          : 64310
   proverCalls         : 13
   memory (bytes)      : 1401946112
   time (s)            : 10.52
   maxProcs            : 4
   statesInstantiated  : 273346
   statesSaved         : 25943
   statesSeen          : 25887
   statesMatched       : 51
   steps               : 37907
   transitions         : 25937

The standard properties hold for all executions.
NAME: heated{\U}plate{\U}openmp.c
CITE: \cite{Quinn:Book04}
TYPE: $\text{O}^r$
SCALE: \texttt{NT=3,M=5,N=5,EPSILON=0.1}

files,language,blank,comment,code,"http://cloc.sourceforge.net v 1.62  T=0.02 s (63.9 files/s, 19176.9 lines/s)"
1,C,44,106,150
civl verify -ompNoSimplify -ompLoopDecomp=ROUND_ROBIN -inputTHREAD_MAX=3 -enablePrintf=false  -DMATH_ELABORATE_ASSUMPTIONS heated_plate_openmp.c
CIVL v0.16 of 2015-1-6 -- http://vsl.cis.udel.edu/civl
19s: mem=1293Mb steps=75201 trans=61696 seen=61545 saved=61747 prove=16

=================== Stats ===================
   validCalls          : 357684
   proverCalls         : 16
   memory (bytes)      : 1266679808
   time (s)            : 30.0
   maxProcs            : 4
   statesInstantiated  : 1018888
   statesSaved         : 107825
   statesSeen          : 107518
   statesMatched       : 260
   steps               : 135671
   transitions         : 107777

The standard properties hold for all executions.
NAME: omp{\U}bug5.c
CITE: \cite{LLNL:OpenMP:URL}
TYPE: $\text{O}$
SCALE: \texttt{NT=3,N=10}

files,language,blank,comment,code,"http://cloc.sourceforge.net v 1.62  T=0.01 s (73.8 files/s, 5907.6 lines/s)"
1,C,8,18,54
civl verify -ompLoopDecomp=ALL -inputTHREAD_MAX=3 -enablePrintf=false  omp_bug5.c
CIVL v0.16 of 2015-1-6 -- http://vsl.cis.udel.edu/civl
Error 0 encountered at depth 1843:
CIVL execution error in p1(id=1) (kind: OTHER, certainty: PROVEABLE)
The second argument of $translate_ptr() &<d22>locka_status doesn't have a compatible type hierarchy as the first argument &<d22>locka_local.lock
at civl-omp.cvl:225.30-66 "$translate_ptr(leaf, shared->status)".
State -1:15097
| Path condition
| | (0 <= SIZEOF(dynamicType<233>)+-1) && (0 <= SIZEOF(dynamicType<241>)+-1) && (0 <= SIZEOF(dynamicType<246>)+-1) && (0 <= SIZEOF(dynamicType<250>)+-1) && (0 <= -1*X3+9) && (0 <= X3+-1)
| Dynamic scopes
| | dyscope d0 (id=0, parent=NULL, static=0)
| | | variables
| | | | _time_count_var = 0
| | | | CIVL_argc = X3
| | | | CIVL_argv = X4
| | | | THREAD_MAX = 3
| | | | $omp_numThreads = 3
| | dyscope d5 (id=1, parent=d1, static=41)
| | | variables
| | | | _heap = 
| | | | | objects of malloc 0 at civl-omp.cvl:71.13-74 "result = ($omp_gteam)$malloc( ... )":
| | | | | | 0: (OMP_gteam[1])<OMP_gteam<d5,1,(boolean[1])<true>,(OMP_work_record[0][])>,(pointer[0])>,&<d5>heap<4,0>[0]>>
| | | | | objects of malloc 2 at civl-omp.cvl:126.15-127.67 "result =\n    ($omp_gshared)$malloc ... )":
| | | | | | 0: (OMP_gshared[1])<OMP_gshared<(boolean[1])<false>,&<d1>a>>
| | | | | | 1: (OMP_gshared[1])<OMP_gshared<(boolean[1])<false>,&<d1>b>>
| | | | | | 2: (OMP_gshared[1])<OMP_gshared<(boolean[1])<false>,&<d1>nthreads>>
| | | | | | 3: (OMP_gshared[1])<OMP_gshared<(boolean[1])<false>,&<d1>locka>>
| | | | | | 4: (OMP_gshared[1])<OMP_gshared<(boolean[1])<false>,&<d1>lockb>>
| | | | | | 5: (OMP_gshared[1])<OMP_gshared<(boolean[1])<false>,&<d1>i>>
| | | | | objects of malloc 4:
| | | | | | 0: (__gbarrier__[1])<__gbarrier__<1,(process[1])<p1>,(boolean[1])<false>,0>>
| | | | _nthreads = 1
| | | | thread_range = $regular_range<0,0,1>
| | | | dom = $domain<1,0,inject(0,($regular_range[1])<$regular_range<0,0,1>>)>
| | | | gteam = &<d5>heap<0,0>[0]
| | | | a_gshared = &<d5>heap<2,0>[0]
| | | | b_gshared = &<d5>heap<2,1>[0]
| | | | nthreads_gshared = &<d5>heap<2,2>[0]
| | | | locka_gshared = &<d5>heap<2,3>[0]
| | | | lockb_gshared = &<d5>heap<2,4>[0]
| | | | i_gshared = &<d5>heap<2,5>[0]
| | | | _dom_size0 = 1
| | | | _par_procs0 = (process[1])<p1>
| | dyscope d1 (id=2, parent=d0, static=39)
| | | variables
| | | | _argv = (pointer[10])<&<d0>CIVL_argv[0][0],&<d0>CIVL_argv[1][0],&<d0>CIVL_argv[2][0],&<d0>CIVL_argv[3][0],&<d0>CIVL_argv[4][0],&<d0>CIVL_argv[5][0],&<d0>CIVL_argv[6][0],&<d0>CIVL_argv[7][0],&<d0>CIVL_argv[8][0],&<d0>CIVL_argv[9][0]>
| | | | argv = &<d1>_argv[0]
| | | | nthreads = 1
| | | | i = NULL
| | | | a = (real[10])<0,63115038377/20000000000,63115038377/10000000000,189345115131/20000000000,63115038377/5000000000,63115038377/4000000000,189345115131/10000000000,441805268639/20000000000,63115038377/2500000000,568035345393/20000000000>
| | | | b = (real[10])<0,6283185307/2000000000,6283185307/1000000000,18849555921/2000000000,6283185307/500000000,6283185307/400000000,18849555921/1000000000,43982297149/2000000000,6283185307/250000000,56548667763/2000000000>
| | | | locka = omp_lock_t<true>
| | | | lockb = omp_lock_t<true>
| | dyscope d22 (id=3, parent=d21, static=77)
| | | variables
| | | | _heap = 
| | | | | objects of malloc 1 at civl-omp.cvl:95.12-71 "result = ($omp_team)$malloc( ... )":
| | | | | | 0: (OMP_team[1])<OMP_team<&<d5>heap<0,0>[0],d22,0,(pointer[6])<&<d22>heap<3,0>[0],&<d22>heap<3,1>[0],&<d22>heap<3,2>[0],&<d22>heap<3,3>[0],&<d22>heap<3,4>[0],&<d22>heap<3,5>[0]>,&<d22>heap<5,0>[0]>>
| | | | | objects of malloc 3 at civl-omp.cvl:145.14-146.64 "result =\n    ($omp_shared)$malloc ... )":
| | | | | | 0: (OMP_shared[1])<OMP_shared<&<d5>heap<2,0>[0],0,&<d22>a_local,&<d22>a_status>>
| | | | | | 1: (OMP_shared[1])<OMP_shared<&<d5>heap<2,1>[0],0,&<d22>b_local,&<d22>b_status>>
| | | | | | 2: (OMP_shared[1])<OMP_shared<&<d5>heap<2,2>[0],0,&<d22>nthreads_local,&<d22>nthreads_status>>
| | | | | | 3: (OMP_shared[1])<OMP_shared<&<d5>heap<2,3>[0],0,&<d22>locka_local,&<d22>locka_status>>
| | | | | | 4: (OMP_shared[1])<OMP_shared<&<d5>heap<2,4>[0],0,&<d22>lockb_local,&<d22>lockb_status>>
| | | | | | 5: (OMP_shared[1])<OMP_shared<&<d5>heap<2,5>[0],0,&<d22>i_local,&<d22>i_status>>
| | | | | objects of malloc 5:
| | | | | | 0: (__barrier__[1])<__barrier__<0,&<d5>heap<4,0>[0]>>
| | | | team = &<d22>heap<1,0>[0]
| | | | a_local = (real[10])<0,0,0,0,0,0,0,0,0,0>
| | | | a_status = (int[10])<0,0,0,0,0,0,0,0,0,0>
| | | | b_local = (real[10])<0,0,0,0,0,0,0,0,0,0>
| | | | b_status = (int[10])<0,0,0,0,0,0,0,0,0,0>
| | | | nthreads_local = 0
| | | | nthreads_status = 0
| | | | locka_local = omp_lock_t<false>
| | | | locka_status = 2
| | | | lockb_local = omp_lock_t<false>
| | | | lockb_status = 2
| | | | i_local = 1
| | | | i_status = 2
| | | | a_shared = &<d22>heap<3,0>[0]
| | | | b_shared = &<d22>heap<3,1>[0]
| | | | nthreads_shared = &<d22>heap<3,2>[0]
| | | | locka_shared = &<d22>heap<3,3>[0]
| | | | lockb_shared = &<d22>heap<3,4>[0]
| | | | i_shared = &<d22>heap<3,5>[0]
| | | | tid$omp_private = 0
| | | | _anon_12 = "Thread %d starting...\n"
| | dyscope d21 (id=4, parent=d5, static=44)
| | | variables
| | | | _tid = 0
| | dyscope d50 (id=5, parent=d0, static=33)
| | | variables
| | | | team = &<d22>heap<1,0>[0]
| | dyscope d55 (id=6, parent=d54, static=64)
| | | variables
| | | | shared = &<d22>heap<3,3>[0]
| | dyscope d54 (id=7, parent=d53, static=63)
| | | variables
| | | | i = 3
| | dyscope d53 (id=8, parent=d52, static=62)
| | | variables
| | | | num_shared = 6
| | dyscope d52 (id=9, parent=d0, static=32)
| | | variables
| | | | team = &<d22>heap<1,0>[0]
| | dyscope d60 (id=10, parent=d59, static=60)
| | | variables
| | | | $sef$2 = NULL
| | dyscope d59 (id=11, parent=d58, static=59)
| | | variables
| | | | leaf = &<d22>locka_local.lock
| | | | leaf_status = NULL
| | | | leaf_shared = NULL
| | dyscope d58 (id=12, parent=d57, static=58)
| | | variables
| | | | i = 0
| | dyscope d57 (id=13, parent=d131, static=57)
| | | variables
| | | | gshared = &<d5>heap<2,3>[0]
| | | | tid = 0
| | | | refs = (pointer[1])<&<d22>locka_local.lock>
| | | | numRefs = 1
| | dyscope d131 (id=14, parent=d0, static=31)
| | | variables
| | | | shared = &<d22>heap<3,3>[0]
| | | | ref = &<d22>locka_local
| Process states
| | process p0(id=0)
| | | call stack
| | | | Frame[function=_CIVL_system, location=27, OpenMPtoCIVLTransformer:0.-1-20 "$parfor(int _tid: ..." inserted by OpenMPtoCIVLTransformer.parallelPragmabefore op.h:22.1-10 "Operation" included from civlc.cvh:12.9-15 "<op.h>" included from omp.cvl:1.9-20 "<civlc.cvh>", dyscope=d5]
| | process p1(id=1)
| | | call stack
| | | | Frame[function=$omp_flush, location=131, civl-omp.cvl:225.30-44 "$translate_ptr", dyscope=d663]
| | | | Frame[function=$omp_flush_all, location=145, civl-omp.cvl:248.5-15 "$omp_flush", dyscope=d55]
| | | | Frame[function=$omp_barrier_and_flush, location=148, civl-omp.cvl:259.2-16 "$omp_flush_all", dyscope=d50]
| | | | Frame[function=_par_proc0, location=334, OpenMPtoCIVLTransformer:0.-1-4 "team\n" inserted by OpenMPtoCIVLTransformer.barrierAndFlushCallbefore op.h:22.1-10 "Operation" included from civlc.cvh:12.9-15 "<op.h>" included from omp.cvl:1.9-20 "<civlc.cvh>", dyscope=d22]

Logging new entry 0, writing trace to CIVLREP/omp_bug5_0.trace

Error bound exceeded: search terminated

=================== Stats ===================
   validCalls          : 11036
   proverCalls         : 9
   memory (bytes)      : 908591104
   time (s)            : 3.46
   maxProcs            : 4
   statesInstantiated  : 15098
   statesSaved         : 1858
   statesSeen          : 1843
   statesMatched       : 0
   steps               : 2218
   transitions         : 1842

The program MAY NOT be correct.  See CIVLREP/omp_bug5_log.txt
