CBMC version 5.54.0 (cbmc-5.54.0) 64-bit x86_64 linux
Parsing BM_cat_v1.c
Converting
Type-checking BM_cat_v1
Generating GOTO Program
Adding CPROVER library (x86_64)
Removal of function pointers and virtual functions
Generic Property Instrumentation
Running with 9 object bits, 55 offset bits (user-specified)
Starting Bounded Model Checking
Unwinding loop search_cat_brute.0 iteration 1 file BM_cat_v1.c line 12 function search_cat_brute thread 0
Unwinding loop search_cat_brute.0 iteration 2 file BM_cat_v1.c line 12 function search_cat_brute thread 0
...
Unwinding loop search_cat_BM_v1.0 iteration 8 file BM_cat_v1.c line 36 function search_cat_BM_v1 thread 0
Not unwinding loop search_cat_BM_v1.0 iteration 9 file BM_cat_v1.c line 36 function search_cat_BM_v1 thread 0
Runtime Symex: 0.0570656s
size of program expression: 1328 steps
simple slicing removed 2 assignments
Generated 2 VCC(s), 2 remaining after simplification
Runtime Postprocess Equation: 0.000101775s
Passing problem to propositional reduction
converting SSA
Runtime Convert SSA: 0.0178482s
Running propositional reduction
Post-processing
Runtime Post-process: 3.0256e-05s
Solving with MiniSAT 2.2.1 with simplifier
13867 variables, 26286 clauses
SAT checker: instance is UNSATISFIABLE
Runtime Solver: 0.0196347s
Runtime decision procedure: 0.0375839s

** Results:
BM_cat_v1.c function check
[check.assertion.1] line 85 assert: SUCCESS

BM_cat_v1.c function search_cat_BM_v1
[search_cat_BM_v1.unwind.0] line 36 unwinding assertion loop 0: SUCCESS

** 0 of 2 failed (1 iterations)
VERIFICATION SUCCESSFUL
CBMC version 5.54.0 (cbmc-5.54.0) 64-bit x86_64 linux
Parsing BM_cat_v2.c
Converting
Type-checking BM_cat_v2
Generating GOTO Program
Adding CPROVER library (x86_64)
Removal of function pointers and virtual functions
Generic Property Instrumentation
Running with 9 object bits, 55 offset bits (user-specified)
Starting Bounded Model Checking
Unwinding loop search_cat_brute.0 iteration 1 file BM_cat_v2.c line 12 function search_cat_brute thread 0
Unwinding loop search_cat_brute.0 iteration 2 file BM_cat_v2.c line 12 function search_cat_brute thread 0
...
Unwinding loop search_cat_BM_v2.0 iteration 7 file BM_cat_v2.c line 36 function search_cat_BM_v2 thread 0
Unwinding loop search_cat_BM_v2.0 iteration 8 file BM_cat_v2.c line 36 function search_cat_BM_v2 thread 0
Not unwinding loop search_cat_BM_v2.0 iteration 9 file BM_cat_v2.c line 36 function search_cat_BM_v2 thread 0
Runtime Symex: 0.0558006s
size of program expression: 1364 steps
simple slicing removed 2 assignments
Generated 2 VCC(s), 2 remaining after simplification
Runtime Postprocess Equation: 0.000102357s
Passing problem to propositional reduction
converting SSA
Runtime Convert SSA: 0.0180041s
Running propositional reduction
Post-processing
Runtime Post-process: 2.8173e-05s
Solving with MiniSAT 2.2.1 with simplifier
14237 variables, 28199 clauses
SAT checker: instance is UNSATISFIABLE
Runtime Solver: 0.0277352s
Runtime decision procedure: 0.0458506s

** Results:
BM_cat_v2.c function check
[check.assertion.1] line 87 assert: SUCCESS

BM_cat_v2.c function search_cat_BM_v2
[search_cat_BM_v2.unwind.0] line 36 unwinding assertion loop 0: SUCCESS

** 0 of 2 failed (1 iterations)
VERIFICATION SUCCESSFUL