// BindingGuardsResolution.dfy


module TypesNotFullyDetermined {
  method T0()
  {
    if x :| true {
    }
  }

  method T1()
  {
    if x :| true {
      var y := x + 3;
    }
  }
}

module Ghost {
  predicate P(x: int)

  predicate method R(x: int)

  method M7() returns (z: int, b: bool)
  {
    if * {
      z := z + -z;
    } else if y :| 1000 <= y < 2000 && R(y) {
      z := y;
    } else if y :| 0 <= y < 100 && P(y) {
      z := y;
    } else if y :| 0 <= y < 100 && R(y) {
      z := y;
    }
    if * {
      z := z + -z;
    } else if exists y :: 1000 <= y < 2000 && R(y) {
      z := 0;
    } else if exists y :: 0 <= y < 100 && P(y) {
      z := 0;
    } else if exists y :: 0 <= y < 100 && R(y) {
      z := 0;
    }
    if P(z) {
      z := 20;
    }
    b := exists y :: 0 <= y < 100 && P(y);
    ghost var c;
    c := exists y :: 0 <= y < 100 && P(y);
    b := exists y {:myattribute P(y)} :: 0 <= y < 100;
  }
}
predicate P(n: int)

predicate R(r: real)

method M0()
{
  if x :| P(x) {
    var y := x + 3;
    var x := true;
  }
}

method M1()
{
  if x: int :| P(x) {
    x := x + 1;
  }
}

method M2()
{
  var x := true;
  if x, y :| P(x) && R(y) {
    var z := x + 12;
  }
  x := x && false;
}

method M3()
{
  var x := true;
  if x: int, y :| P(x) && R(y) {
    var z := x + int(y);
    var w := real(x) + y;
  }
  var x := 0.0;
}

method M4()
{
  if x, y: real :| P(x) && R(y) {
  }
}

method M5()
{
  if x: int, y: real :| P(x) && R(y) {
  }
}

method M6()
{
  if x {:myattribute x, "hello"} :| P(x) {
  }
  if x, y {:myattribute y, "sveika"} :| P(x) && R(y) {
  }
  if x: int {:myattribute x, "chello"} :| P(x) {
  }
  if x {:myattribute x, "hola"} {:yourattribute x + x, "hej"} :| P(x) {
  }
}

method M7()
{
  if x :| P(x) {
  } else if * {
  } else if y :| R(y) {
  } else if y :| P(y) {
  }
}

method P0(m: int, n: int)
  requires m < n
{
  var x := true;
  if {
    case x :| P(x) =>
      var t := 3 * x;
    case x: int :| P(x) =>
    case x, y :| P(x) && R(y) =>
      y := y + 1.0;
    case x: int, y :| P(x) && R(y) =>
    case m < n =>
      x := x || m + 5 == n;
    case x, y: real :| P(x) && R(y) =>
    case x: int, y: real :| P(x) && R(y) =>
  }
  assert x;
}

method P1(m: int, n: int)
  requires m < n
{
  if {
    case x {:myattribute x, "hello"} :| P(x) =>
    case x, y {:myattribute y, "sveika"} :| P(x) && R(y) =>
    case x: int {:myattribute x, "chello"} :| P(x) =>
    case x {:myattribute x, "hola"} {:yourattribute x + x, "hej"} :| P(x) =>
    case m < n =>
  }
}
BindingGuardsResolution.dfy(109,7): Error: type of bound variable 'x' could not be determined; please specify the type explicitly
BindingGuardsResolution.dfy(130,8): Error: Assignment to non-ghost variable is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
BindingGuardsResolution.dfy(132,8): Error: Assignment to non-ghost variable is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
BindingGuardsResolution.dfy(140,8): Error: Assignment to non-ghost variable is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
BindingGuardsResolution.dfy(142,8): Error: Assignment to non-ghost variable is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
BindingGuardsResolution.dfy(146,8): Error: Assignment to non-ghost variable is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
BindingGuardsResolution.dfy(149,37): Error: function calls are allowed only in specification contexts (consider declaring the function a 'function method')
BindingGuardsResolution.dfy(12,8): Error: Duplicate local-variable name: x
BindingGuardsResolution.dfy(19,4): Error: LHS of assignment must denote a mutable variable
BindingGuardsResolution.dfy(39,6): Error: Duplicate local-variable name: x
BindingGuardsResolution.dfy(84,6): Error: LHS of assignment must denote a mutable variable
11 resolution/type errors detected in BindingGuardsResolution.dfy