Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Inconsistency in the results by different SMT solvers #8300

Open
ArpitaDutta opened this issue May 21, 2024 · 3 comments
Open

Inconsistency in the results by different SMT solvers #8300

ArpitaDutta opened this issue May 21, 2024 · 3 comments

Comments

@ArpitaDutta
Copy link

For the following program, I am getting different results from different solvers. Bug is unreachable in the program however some of the solvers states it as reachable.

#include <stdio.h>
#include <stdlib.h>
#include <assert.h>

#define loop for(;;)

#define ipoint(var) { int var=nondet_int(); if (var) goto END; }

main() {
	int x=0;
		
		int choice =nondet_int();
		if (choice) {
           		x=x+1; 
        	} 
		else {	
			x=x+2;
		}
		if (x==5) __CPROVER_assert(0,"Bug at this point");
}

Output for cbmc undCBMCSmall.c --z3 OR cbmc undCBMCSmall.c --cvc3 OR cbmc undCBMCSmall.c --smt2 is as follows:

CBMC version 5.80.0 (cbmc-5.80.0) 64-bit x86_64 linux
Parsing undCBMCSmall.c
Converting
Type-checking undCBMCSmall
file undCBMCSmall.c line 13 function main: function 'nondet_int' is not declared
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
Runtime Symex: 0.000688196s
size of program expression: 36 steps
simple slicing removed 6 assignments
Generated 1 VCC(s), 1 remaining after simplification
Runtime Postprocess Equation: 1.1761e-05s
Passing problem to propositional reduction
converting SSA
Runtime Convert SSA: 0.000164315s
Running propositional reduction
Post-processing
Runtime Post-process: 3.815e-06s
Solving with MiniSAT 2.2.1 with simplifier
164 variables, 133 clauses
SAT checker inconsistent: instance is UNSATISFIABLE
Runtime Solver: 2.3411e-05s
Runtime decision procedure: 0.000216109s

** Results:
undCBMCSmall.c function main
[main.assertion.1] line 20 Bug at this point: SUCCESS

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

Where for cbmc undCBMCSmall.c --cvc4 OR cbmc undCBMCSmall.c --cvc5 OR cbmc undCBMCSmall.c --yices OR cbmc undCBMCSmall.c --cprover-smt2 OR cbmc undCBMCSmall.c --boolector OR cbmc undCBMCSmall.c --cprover-bitwuzla OR cbmc undCBMCSmall.c --cprover-mathsat is as follows:

CBMC version 5.80.0 (cbmc-5.80.0) 64-bit x86_64 linux
Parsing undCBMCSmall.c
Converting
Type-checking undCBMCSmall
file undCBMCSmall.c line 13 function main: function 'nondet_int' is not declared
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
Runtime Symex: 0.000728194s
size of program expression: 36 steps
simple slicing removed 6 assignments
Generated 1 VCC(s), 1 remaining after simplification
Runtime Postprocess Equation: 1.4794e-05s
Passing problem to SMT2 ALL using CVC4
converting SSA
Runtime Convert SSA: 0.000153958s
Running SMT2 ALL using CVC4
Runtime Solver: 0.00277197s
Runtime decision procedure: 0.00298569s

** Results:
undCBMCSmall.c function main
[main.assertion.1] line 20 Bug at this point: ERROR

** 0 of 1 failed (1 iterations)
VERIFICATION ERROR

CBMC version: 5.80.0 (cbmc-5.80.0)
Operating system: Ubuntu 16.04 / macOS Sonoma Version 14.3
Exact command line resulting in the issue: cbmc programname.c --cvc5/ --cvc3/ --cvc4 / .. other SMT solvers
What behaviour did you expect: expecting same behavior from all SMT solvers as "VERIFICATION SUCCESSFUL" since the bug is unreachable
What happened instead: Different solvers gives different results

@martin-cs
Copy link
Collaborator

Please forgive me if this question is patronising or stupid but ... do you have all of these solvers installed and on the command-line path? CBMC does not build them in, you have to install them separately.

@kroening
Copy link
Member

Please forgive me if this question is patronising or stupid but ... do you have all of these solvers installed and on the command-line path? CBMC does not build them in, you have to install them separately.

We should add a "solver executable not found, please install" message.

@tautschnig
Copy link
Collaborator

I believe #8378 will also address this one.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

4 participants