ERROR. Program invariants were NOT detected with PAGAI

[lucasccordeiro]

main.zip

lucascordeiro@lucascordeiro:~/depthk-depthk_v3$ python depthk.py ~/esbmc-private/regression/esbmc/01_cbmc_abs1/main.c -g

Running PAGAI to generate the invariants
Running PAGAI translation
ERROR. Program invariants were NOT detected with PAGAI
Starting the verification of the P' program
-> Actual k = 1
Status: checking base case
Status: checking forward condition
v> Forcing last check in base case
Status: checking inductive step
> Forcing last check in base case
-> Actual k = 2
Status: checking base case

Running CPAchecker with default heap size (1200M). Specify a larger value with -heap if you have more RAM.
Running CPAchecker with default stack size (1024k). Specify a larger value with -stack if needed.
Error: Invalid configuration (Please specify a program to analyze on the command line.) (CPAMain.main, SEVERE)

     Last adopted - Status: checking inductive step

UNKNOWN

[WilliameRocha]

O problema ocorreu pq o arquivo de propriedades não foi passado como parâmetro, e como o resultado foi TRUE o CPAchecker foi acionado

[lucasccordeiro]

@WilliameRocha and @hbgit: I believe that this error should not occur if we call the script depthk.py, right?