SATABS breaks unexpected in CProver Analysis
The CProver analysis based on SatABS fails, at least in some cases.
The SatABS output looks like this:
file src-gen/Behavior_ID_64.c: Parsing
file src-gen/Controller_ID_63.c: Parsing
file src-gen/data_dictionary.c: Parsing
file src-gen/cProver_analysis_entry.c: Parsing
Converting
Type-checking Behavior_ID_64
Type-checking Controller_ID_63
Type-checking cProver_analysis_entry
Type-checking data_dictionary
Generating GOTO Program
Adding CPROVER library
48 functions, 561 instructions.
Removing function pointers
Removing unused functions
Dropping 10 of 48 functions (38 used)
Full inlining
*** Starting CEGAR Loop ***
Calculating initial set of predicates
*** CEGAR Loop Iteration 1
Computing Predicate Abstraction for Program
Running BOOM
boom --stats -t --threadbound 5 cegar_tmp_abstract.bp >cegar_tmp_boolean_program_out1 2>cegar_tmp_boolean_program_out2
unexpected result from Boom
This error can be reproduced by the following JUnit-Test Cases:
- ‘testSATABSCounterexample’ in class StructEnumArrayCProverBasedAnalyzerTest.scala
- ‘allPermutationsTest’ in class CProverAnalysisParametersTest.scala
(Analyses on the Simple TLC fail in the same way…)
(from redmine: issue id 2408, created on 2015-08-06, closed on 2017-11-28)