File tree Expand file tree Collapse file tree 2 files changed +3
-4
lines changed
Test/civl/regression-tests Expand file tree Collapse file tree 2 files changed +3
-4
lines changed Original file line number Diff line number Diff line change @@ -874,7 +874,7 @@ public Element TryGet(string varname)
874874 public void AddBinding ( string varname , Element value )
875875 {
876876 vars . Add ( varname ) ;
877- valuations . Add ( varname , value ) ;
877+ valuations . Add ( varname , value ) ; // SQ: exception occurs if a global variable and a local variable have the same name
878878 }
879879
880880 // Change name of the state
Original file line number Diff line number Diff line change 11// RUN: %parallel-boogie "%s" > "%t"
22// RUN: %diff "%s.expect" "%t"
3- // UNSUPPORTED: batch_mode
43
54var {:layer 0 ,2 } x : int;
65
@@ -33,7 +32,7 @@ asserts {:add_to_pool "A", i+1} true;
3332 assume j > i;
3433}
3534
36- pure action intro (x: int)
35+ pure action intro (k: int)
3736{
38- assume x == 0 ;
37+ assume k == 0 ;
3938}
You can’t perform that action at this time.
0 commit comments