Skip to content

Issue when using delphi as the solver #264

@ktpss97094

Description

@ktpss97094

I used the default solver to run the following minimal example:
$ uclid min_smto_bug.ucl

module main {
  var step : integer;
  init { step = 0; }
  next { step' = step + 1; }
  invariant test : step != 1;
  control {
    v = bmc(2);
    print_results;
  }
}

gives the expected output:

Successfully instantiated 1 module(s).
2 assertions passed.
1 assertions failed.
0 assertions indeterminate.
  PASSED -> v [Step #0] property test @ min_smto_bug.ucl, line 5
  PASSED -> v [Step #2] property test @ min_smto_bug.ucl, line 5
  FAILED -> v [Step #1] property test @ min_smto_bug.ucl, line 5
Finished execution for module: main.

But used the delphi solver to run the same example:
$ uclid -s "delphi --smto" min_smto_bug.ucl

gives the unexpected output:

Successfully instantiated 1 module(s).
3 assertions passed.
0 assertions failed.
0 assertions indeterminate.
  PASSED -> v [Step #0] property test @ min_smto_bug.ucl, line 5
  PASSED -> v [Step #1] property test @ min_smto_bug.ucl, line 5
  PASSED -> v [Step #2] property test @ min_smto_bug.ucl, line 5
Finished execution for module: main.

I'm wondering whether there's an issue with the delphi solver or if I'm using it incorrectly. I use the delphi solver because I want to use oracle functions. Thanks.

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions