NAME: diffusion1d.c
CITE: \cite{siegel-zirkel:2011:fevs-mcs}
SCALE: {\texttt{NPin1,3], NSTEPS, NXin1,5]}}
civl verify -enablePrintf=false -collectHeaps=false diffusion1d.c
CIVL v1.7.1+ of 2016-05-31 -- http://vsl.cis.udel.edu/civl
19s: mem=2450Mb trans=77659 traceSteps=36852 explored=78463 saved=36854 prove=232
34s: mem=3015Mb trans=152266 traceSteps=68635 explored=154199 saved=68636 prove=275

=== Command ===
civl verify -enablePrintf=false -collectHeaps=false diffusion1d.c 

=== Stats ===
   time (s)            : 33.43
   memory (bytes)      : 3161980928
   max process count   : 4
   states              : 156479
   states saved        : 69557
   state matches       : 0
   transitions         : 154517
   trace steps         : 69556
   valid calls         : 605582
   provers             : z3, cvc4
   prover calls        : 276

=== Result ===
The standard properties hold for all executions.
NAME: diffusion2d.c
CITE: \cite{siegel-zirkel:2011:fevs-mcs}
SCALE: {\texttt{NPX=NPY=2, NSTEPS, NX, NYin1,5]}}
civl verify -enablePrintf=false -collectHeaps=false diffusion2d.c
CIVL v1.7.1+ of 2016-05-31 -- http://vsl.cis.udel.edu/civl
19s: mem=2450Mb trans=29940 traceSteps=12076 explored=30340 saved=12077 prove=61
34s: mem=3017Mb trans=71190 traceSteps=28807 explored=72135 saved=28808 prove=78
49s: mem=2611Mb trans=115427 traceSteps=46647 explored=116934 saved=46648 prove=78
64s: mem=2403Mb trans=158657 traceSteps=63838 explored=160765 saved=63839 prove=78
79s: mem=2049Mb trans=204354 traceSteps=81777 explored=207091 saved=81778 prove=78
94s: mem=1820Mb trans=254073 traceSteps=101167 explored=257494 saved=101168 prove=78
109s: mem=1545Mb trans=310463 traceSteps=122897 explored=314616 saved=122898 prove=78
124s: mem=1236Mb trans=367380 traceSteps=145006 explored=372216 saved=145007 prove=96
139s: mem=976Mb trans=414999 traceSteps=164351 explored=420497 saved=164352 prove=105
154s: mem=719Mb trans=465109 traceSteps=184500 explored=471319 saved=184501 prove=105
169s: mem=562Mb trans=515777 traceSteps=204603 explored=522719 saved=204604 prove=105
184s: mem=668Mb trans=566801 traceSteps=224632 explored=574500 saved=224633 prove=105
199s: mem=839Mb trans=635776 traceSteps=251964 explored=644192 saved=251965 prove=123

=== Command ===
civl verify -enablePrintf=false -collectHeaps=false diffusion2d.c 

=== Stats ===
   time (s)            : 207.22
   memory (bytes)      : 1253572608
   max process count   : 5
   states              : 699656
   states saved        : 273987
   state matches       : 0
   transitions         : 690734
   trace steps         : 273986
   valid calls         : 3353858
   provers             : z3, cvc4
   prover calls        : 123

=== Result ===
The standard properties hold for all executions.
NAME: diffusion2d.c
CITE: 
SCALE: {\texttt{NPX=NX=3,NPY=NY=1,NSTEPS=2}}
civl verify -enablePrintf=false -collectHeaps=false -inputny=1 -inputnsteps=2 -inputnx=3  -inputNPROCSX=3 -inputNPROCSY=1 diffusion2d.c
CIVL v1.7.1+ of 2016-05-31 -- http://vsl.cis.udel.edu/civl

=== Command ===
civl verify -enablePrintf=false -collectHeaps=false -inputny=1 -inputnsteps=2 -inputnx=3 -inputNPROCSX=3 -inputNPROCSY=1 diffusion2d.c 

=== Stats ===
   time (s)            : 4.34
   memory (bytes)      : 919076864
   max process count   : 4
   states              : 2870
   states saved        : 1163
   state matches       : 0
   transitions         : 2838
   trace steps         : 1162
   valid calls         : 12254
   provers             : z3, cvc4
   prover calls        : 3

=== Result ===
The standard properties hold for all executions.
NAME: wave1d.c
CITE: \cite{Dummy}
SCALE: {\texttt{NPin1,4], NSTEPS,NXin1,5]}}
civl verify -enablePrintf=false -collectHeaps=false wave1d.c
CIVL v1.7.1+ of 2016-05-31 -- http://vsl.cis.udel.edu/civl
19s: mem=2457Mb trans=75458 traceSteps=32550 explored=76535 saved=32551 prove=40

=== Command ===
civl verify -enablePrintf=false -collectHeaps=false wave1d.c 

=== Stats ===
   time (s)            : 30.01
   memory (bytes)      : 3157786624
   max process count   : 5
   states              : 127159
   states saved        : 52063
   state matches       : 0
   transitions         : 125234
   trace steps         : 52062
   valid calls         : 532622
   provers             : z3, cvc4
   prover calls        : 40

=== Result ===
The standard properties hold for all executions.
NAME: wave1dBad.c
CITE: \cite{Dummy}
SCALE: {\texttt{NPin1,4], NSTEPS,NXin1,5]}}
civl verify -enablePrintf=false -collectHeaps=false wave1dBad.c
CIVL v1.7.1+ of 2016-05-31 -- http://vsl.cis.udel.edu/civl


Violation 0 encountered at depth 264:
CIVL execution violation in p1 (kind: ASSERTION_VIOLATION, certainty: PROVEABLE)
at wave1dBad.c:208.5-210.60 "$assert((oracle[time +  ... )":

Assertion: (((oracle)[(time+1)])[((first+i)+1)]==*((buf+i)))
        -> -2*(((((X_u_init[1]+((-1/2)*X_u_init[2])+((-1/2)*X_u_init[0]))*(X_c^2))+((X_u_init[1]+(-2*X_u_init[0]))*(X_c^2))+((-1/2)*X_u_init[1])+X_u_init[0])*(X_c^2))+(-1*((X_u_init[1]+(-2*X_u_init[0]))*(X_c^2)))+((-1/2)*X_u_init[0]))==*(&<d2>heap.malloc6[0][1]+0)
        -> (-2*(((((X_u_init[1]+((-1/2)*X_u_init[2])+((-1/2)*X_u_init[0]))*(X_c^2))+((X_u_init[1]+(-2*X_u_init[0]))*(X_c^2))+((-1/2)*X_u_init[1])+X_u_init[0])*(X_c^2))+(-1*((X_u_init[1]+(-2*X_u_init[0]))*(X_c^2)))+((-1/2)*X_u_init[0])))==(-2*(((((X_u_init[1]+((-1/2)*X_u_init[2])+((-1/2)*X_u_init[0]))*(X_c^2))+((X_u_init[1]+(-2*X_u_init[0]))*(X_c^2))+((-1/2)*X_u_init[1])+X_u_init[0]+((-1/2)*Hp1s2f8o0[0]))*(X_c^2))+(-1*((X_u_init[1]+(-2*X_u_init[0]))*(X_c^2)))+((-1/2)*X_u_init[0])))
        -> (0==((X_u_init[1] + (-1/2)*X_u_init[2] + (-1/2)*X_u_init[0])*(X_c^2) + (X_u_init[1] - 2*X_u_init[0])*(X_c^2) + (-1/2)*X_u_init[1] + X_u_init[0] + (-1/2)*Hp1s2f8o0[0] - 1*((X_u_init[1] + (-1/2)*X_u_init[2] + (-1/2)*X_u_init[0])*(X_c^2) + (X_u_init[1] - 2*X_u_init[0])*(X_c^2) + (-1/2)*X_u_init[1] + X_u_init[0])))||(0==X_c)

Input:
  _civl_argc=X__civl_argc
  _civl_argv=X__civl_argv
  NXB=5
  nx=5
  c=X_c
  NSTEPSB=5
  nsteps=5
  wstep=1
  u_init=X_u_init
  _mpi_nprocs=1
  _mpi_nprocs_lo=1
  _mpi_nprocs_hi=4
Context:
  0<X_c
  0<=(SIZEOF(418)-1)
  0<=(SIZEOF(426)-1)
  0<=(SIZEOF(459)-1)
  0<=(SIZEOF(462)-1)
  0<=(SIZEOF(466)-1)
  0<=(SIZEOF(469)-1)
  0<=(SIZEOF_REAL-1)
  0<=(X__civl_argc-1)
Call stacks:
process 0:
  main at MPITransformer "$parfor (int i: 0 .." inserted by MPITransformer.$parfor MPI_Process before wave1dBad.c:246.13-16 "argc"
process 1:
  printData at wave1dBad.c:208.5-11 "$assert" called from
  write_frame at wave1dBad.c:224.4-12 "printData" called from
  _civl_main at wave1dBad.c:270.6-16 "write_frame" called from
  _mpi_process at GeneralTransformer "_civl_argc, (char*[_" inserted by GeneralTransformer.new main function before wave1dBad.c:246.13-16 "argc" called from
  _par_proc0 at MPITransformer "i" inserted by MPITransformer.function call _mpi_process before wave1dBad.c:246.13-16 "argc"

Logging new entry 0, writing trace to CIVLREP/wave1dBad_0.trace
Terminating search after finding 1 violation.

=== Command ===
civl verify -enablePrintf=false -collectHeaps=false wave1dBad.c 

=== Stats ===
   time (s)            : 4.53
   memory (bytes)      : 919076864
   max process count   : 2
   states              : 505
   states saved        : 264
   state matches       : 0
   transitions         : 504
   trace steps         : 263
   valid calls         : 3038
   provers             : z3, cvc4
   prover calls        : 41

=== Result ===
The program MAY NOT be correct.  See CIVLREP/wave1dBad_log.txt
NAME: gaussJordan_elimination.c
CITE: \cite{siegel-zirkel:2011:fevs-mcs}
SCALE: {\texttt{NPin1,3], ROWin1,COL], COLin1,3]}}
civl verify -enablePrintf=false -collectHeaps=false gaussJordan_elimination.c
CIVL v1.7.1+ of 2016-05-31 -- http://vsl.cis.udel.edu/civl
19s: mem=2451Mb trans=45538 traceSteps=22527 explored=45784 saved=22515 prove=92
34s: mem=2837Mb trans=99272 traceSteps=49145 explored=99798 saved=49125 prove=172
49s: mem=2501Mb trans=154918 traceSteps=76723 explored=155739 saved=76690 prove=252
64s: mem=2210Mb trans=212361 traceSteps=105311 explored=213484 saved=105270 prove=318
79s: mem=1960Mb trans=270109 traceSteps=133987 explored=271536 saved=133938 prove=374
94s: mem=1622Mb trans=328831 traceSteps=163133 explored=330572 saved=163074 prove=433

=== Command ===
civl verify -enablePrintf=false -collectHeaps=false gaussJordan_elimination.c 

=== Stats ===
   time (s)            : 97.76
   memory (bytes)      : 1639972864
   max process count   : 4
   states              : 349869
   states saved        : 172459
   state matches       : 67
   transitions         : 348016
   trace steps         : 172525
   valid calls         : 2262104
   provers             : z3, cvc4
   prover calls        : 441

=== Result ===
The standard properties hold for all executions.
NAME: matmat_mw.c
CITE: \cite{Dummy}
SCALE: {\texttt{NPin2,4], N,L,Min1,3]}}
cd matmat_mw/ && make
civl verify -enablePrintf=false -input_mpi_nprocs_lo=2 -input_mpi_nprocs_hi=4 -inputNB=3 -inputLB=3 -inputMB=3 matmat_mw.c
CIVL v1.7.1+ of 2016-05-31 -- http://vsl.cis.udel.edu/civl
18s: mem=2452Mb trans=76635 traceSteps=30973 explored=77515 saved=30891 prove=29

=== Command ===
civl verify -enablePrintf=false -input_mpi_nprocs_lo=2 -input_mpi_nprocs_hi=4 -inputNB=3 -inputLB=3 -inputMB=3 matmat_mw.c 

=== Stats ===
   time (s)            : 18.98
   memory (bytes)      : 2571108352
   max process count   : 5
   states              : 82772
   states saved        : 32997
   state matches       : 90
   transitions         : 81841
   trace steps         : 33086
   valid calls         : 604728
   provers             : z3, cvc4
   prover calls        : 29

=== Result ===
The standard properties hold for all executions.
NAME: mpi_pi_send.c
CITE: \cite{Dummy}
SCALE: {\texttt{ROUNDS, DARTS, NPin1,2]}}
civl verify -enablePrintf=false -collectHeaps=false mpi_pi_send.c
CIVL v1.7.1+ of 2016-05-31 -- http://vsl.cis.udel.edu/civl
19s: mem=1418Mb trans=67606 traceSteps=27143 explored=68171 saved=27144 prove=651

=== Command ===
civl verify -enablePrintf=false -collectHeaps=false mpi_pi_send.c 

=== Stats ===
   time (s)            : 30.95
   memory (bytes)      : 2564292608
   max process count   : 3
   states              : 135895
   states saved        : 54172
   state matches       : 0
   transitions         : 134765
   trace steps         : 54171
   valid calls         : 514412
   provers             : z3, cvc4
   prover calls        : 1240

=== Result ===
The standard properties hold for all executions.
NAME: mpi_prime.c
CITE: \cite{Dummy}
SCALE: {\texttt{NPin1,4], PRIMESin10,15]}}
civl verify -enablePrintf=false -collectHeaps=false mpi_prime.c
CIVL v1.7.1+ of 2016-05-31 -- http://vsl.cis.udel.edu/civl
19s: mem=876Mb trans=14109 traceSteps=6423 explored=14031 saved=6344 prove=166
34s: mem=1423Mb trans=38197 traceSteps=17400 explored=37955 saved=17155 prove=314

=== Command ===
civl verify -enablePrintf=false -collectHeaps=false mpi_prime.c 

=== Stats ===
   time (s)            : 35.72
   memory (bytes)      : 1492647936
   max process count   : 5
   states              : 46563
   states saved        : 21010
   state matches       : 252
   transitions         : 46810
   trace steps         : 21261
   valid calls         : 178556
   provers             : z3, cvc4
   prover calls        : 326

=== Result ===
The standard properties hold for all executions.
NAME: mpithread_both.c
CITE: \cite{Dummy}
SCALE: {\text{NP=2, THREADSin1,2], VECLEN=5}}
civl verify -enablePrintf=false -collectHeaps=false -inputVECLEN=5 -inputMAXTHRDS=2 -input_mpi_nprocs=2 mpithreads_both.c
CIVL v1.7.1+ of 2016-05-31 -- http://vsl.cis.udel.edu/civl
19s: mem=2446Mb trans=74690 traceSteps=32570 explored=63260 saved=21137 prove=1

=== Command ===
civl verify -enablePrintf=false -collectHeaps=false -inputVECLEN=5 -inputMAXTHRDS=2 -input_mpi_nprocs=2 mpithreads_both.c 

=== Stats ===
   time (s)            : 27.64
   memory (bytes)      : 3163553792
   max process count   : 7
   states              : 109868
   states saved        : 37550
   state matches       : 17161
   transitions         : 127027
   trace steps         : 54710
   valid calls         : 365645
   provers             : z3, cvc4
   prover calls        : 1

=== Result ===
The standard properties hold for all executions.
