diff --git a/regression/goto-analyzer/constant_propagation_08/main.c b/regression/goto-analyzer/constant_propagation_08/main.c index 9bc63eda848..8fb398f3e57 100644 --- a/regression/goto-analyzer/constant_propagation_08/main.c +++ b/regression/goto-analyzer/constant_propagation_08/main.c @@ -5,10 +5,17 @@ int main() int i; i = 0; +#ifndef _WIN64 if (i==0) - a[0]=1; + a[0l] = 1; else - a[1]=2; + a[1l] = 2; +#else + if(i == 0) + a[0ll] = 1; + else + a[1ll] = 2; +#endif __CPROVER_assert(a[0] == 1 || a[1] == 2, "a[0]==1 || a[1]==2"); diff --git a/regression/goto-analyzer/constant_propagation_08/test-vsd.desc b/regression/goto-analyzer/constant_propagation_08/test-vsd.desc index 922c1e85ddc..deb711fa835 100644 --- a/regression/goto-analyzer/constant_propagation_08/test-vsd.desc +++ b/regression/goto-analyzer/constant_propagation_08/test-vsd.desc @@ -3,7 +3,7 @@ main.c --variable-sensitivity --vsd-arrays every-element --simplify out.gb ^EXIT=0$ ^SIGNAL=0$ -^Simplified: assert: 1, assume: 0, goto: 1, assigns: [12], function calls: 0$ -^Unmodified: assert: 0, assume: 0, goto: 2, assigns: [89], function calls: 2$ +^Simplified: assert: 1, assume: 0, goto: 1, assigns: 1, function calls: 0$ +^Unmodified: assert: 0, assume: 0, goto: 2, assigns: 9, function calls: 2$ -- ^warning: ignoring