button spec causes specific trace to fail

[ftc]

Tested on commit 694eebb39ce174a2484365398f1e5bf83ac809ca crashes on input of the following under bmc checking. It does not crash when running check-files and the crash appears to be something to do with grounding. ncs.zip

$ python driver.py -t /home/s/Documents/data/345ab4b1ca978f54b10f14d4898f592001240aa2/ContractionTimerDistilledFix/nocrashsequence.out -m bmc -s /home/s/Documents/source/callback-verification/cbverifier/android_specs/button.spec -k 4

Traceback (most recent call last): File "driver.py", line 195, in main() File "driver.py", line 141, in main ts_enc = TSEncoder(trace, spec_list) File "/home/s/Documents/source/callback-verification/cbverifier/encoding/encoder.py", line 220, in init self.ground_specs = self._compute_ground_spec() File "/home/s/Documents/source/callback-verification/cbverifier/encoding/encoder.py", line 254, in _compute_ground_spec tmp = self.gs.ground_spec(spec) File "/home/s/Documents/source/callback-verification/cbverifier/encoding/grounding.py", line 43, in ground_spec bindings = self._get_ground_bindings(spec) File "/home/s/Documents/source/callback-verification/cbverifier/encoding/grounding.py", line 265, in _get_ground_bindings binding_set = self._ground_bindings_rec(spec.ast, all_bindings) File "/home/s/Documents/source/callback-verification/cbverifier/encoding/grounding.py", line 285, in _ground_bindings_rec return self._ground_bindings_rec(spec_node[1], bindings) File "/home/s/Documents/source/callback-verification/cbverifier/encoding/grounding.py", line 282, in _ground_bindings_rec bindings)) File "/home/s/Documents/source/callback-verification/cbverifier/encoding/grounding.py", line 294, in _ground_bindings_rec res = bindings.combine(spec_res) File "/home/s/Documents/source/callback-verification/cbverifier/encoding/grounding.py", line 485, in combine new_a = assignments.intersect(assignments_other) File "/home/s/Documents/source/callback-verification/cbverifier/encoding/grounding.py", line 370, in intersect if other_map[key] == value: File "/home/s/Documents/source/callback-verification/cbverifier/traces/ctrace.py", line 291, in eq return (self.is_null == other.is_null and AttributeError: 'AssignmentsBottom' object has no attribute 'is_null'

[smover]

@ftc can you add the files to reproduce the crash? (trace + specifications)

[ftc]

The file ncs.zip in the origional post contains the trace and the spec is in the commit mentioned. Sorry for the ambiguity.