cuplv / verivita

Dynamic verification using callbacks
2 stars 1 forks source link

verification takes a long time on something I think should be simple #193

Open ftc opened 7 years ago

ftc commented 7 years ago

command:

-m
ic3
-t
/Users/s/Documents/source/scratch/callback-verification/tests/realApplications/ContractionTimer/bug/trace_140117_0
-s
/Users/s/Documents/source/callback-verification/cbverifier/android_specs/enabledisable/android.app.Fragment/Fragment_combined.spec:/Users/s/Documents/source/callback-verification/cbverifier/android_specs/allowdisallow/fragment/fragment_startActivity.spec:/Users/s/Documents/source/callback-verification/cbverifier/android_specs/allowdisallow/android.support.v4.app.Fragment/fragment_startActivity.spec:/Users/s/Documents/source/callback-verification/cbverifier/android_specs/enabledisable/android.widget.ListView/listView_setListener.spec
--ic3_frames
40
-n
/Users/s/software/nuXmv-1.1.1-Darwin/bin/nuXmv
-z

files:

stateExpl_stateExpl_stateExpl.zip

smover commented 7 years ago

@ftc Can you send me the two different specification files fragment_startActivity.spec?

I see two files with the same name in the command line but I have just one (and I don't know which one) in the zip:

/Users/s/Documents/source/callback-verification/cbverifier/android_specs/allowdisallow/fragment/fragment_startActivity.spec
/Users/s/Documents/source/callback-verification/cbverifier/android_specs/allowdisallow/android.support.v4.app.Fragment/fragment_startActivity.spec

I think they have the same name, so one overwrote the other in the archive

ftc commented 7 years ago

startActivity.zip