Generate SMT-LIB

[MJJ-Shuai]

Hello, my question is: When I use the above command below to convert my C++ code to SMT-LIB code, I find that I cannot find the assert I defined in the generated SMT2 file. It seems that cbmc has hidden it. If I want to see the details of SMT-LIB (with assert, declare, etc.), I will be able to use this command. What instructions should I use?

PS F:\Project\circomjs-starter-main\circuits\multiply_cpp> cbmc --no-sat-preprocessor --cvc5 --outfile multiply.smt2 file1.cpp
CBMC version 5.95.1 (cbmc-5.95.1) 64-bit x86_64 windows
Parsing file1.cpp
file1.cpp
Converting
Type-checking file1
Generating GOTO Program
Adding CPROVER library (x86_64)
Removal of function pointers and virtual functions
Generic Property Instrumentation
Running with 8 object bits, 56 offset bits (default)
Starting Bounded Model Checking
Outputting SMTLib formula to file: multiply.smt2
Runtime Symex: 0.0003849s
size of program expression: 28 steps
simple slicing removed 5 assignments
Generated 1 VCC(s), 1 remaining after simplification
Runtime Postprocess Equation: 0.000191s
Passing problem to SMT2
converting SSA
Runtime Convert SSA: 8.05e-05s
Running SMT2
Runtime Solver: 6.26e-05s
Runtime decision procedure: 0.0004194s

SMT-LIB:

; SMT 2
; Generated for CVC 5
(set-info :source "Generated by CBMC 5.95.1 (cbmc-5.95.1)")
(set-option :produce-models true)
(set-logic ALL)

[tautschnig]

Given "Generated 1 VCC(s), 1 remaining after simplification" I am very much surprised that the above is all the output you got. Would you mind sharing file1.cpp to enable debugging of this?

[MJJ-Shuai]

Given "Generated 1 VCC(s), 1 remaining after simplification" I am very much surprised that the above is all the output you got. Would you mind sharing file1.cpp to enable debugging of this?

Thanks for your reply, this is my cpp code, which is very simple. My purpose is to generate the SMT model corresponding to C++, so I consider using CBMC, hoping that it can meet my needs：

#include <cassert>

int main() {
    int a, b;
    a = 1 + 1;
    b = 1 + 2;
    assert(a + b > 2); 

    return 0;
}

[ArpitaDutta]

@MJJ-Shuai, on running the above program, I got the following output:

CBMC version 5.80.0 (cbmc-5.80.0) 64-bit x86_64 linux
Parsing check.c
Converting
Type-checking check
Generating GOTO Program
Adding CPROVER library (x86_64)
Removal of function pointers and virtual functions
Generic Property Instrumentation
Running with 8 object bits, 56 offset bits (default)
Starting Bounded Model Checking
Outputting SMTLib formula to file: multiply.smt2
Runtime Symex: 0.000414241s
size of program expression: 23 steps
simple slicing removed 0 assignments
Generated 1 VCC(s), 0 remaining after simplification
Runtime Postprocess Equation: 9.946e-06s

The program is simple enough and there is no non determinism here. So the VCC gets simplified.

The output you are getting on multiply.smt2 is correct.

[MJJ-Shuai]

@ArpitaDutta Thanks for your reply, but my purpose is to generate the SMT formula corresponding to C++, so I wonder if CBMC can generate SMT formulas for C++？