output.txt

$ python2 ../cuter -r -s 3 sm multi_step "[{0,[]},[]]" --depth 20
Compiling sm.erl ... ok
Testing sm:multi_step/2 ...
.xx..xx..x.xxx.xxx.xxxxx.xxxxxxxxxxxxxxxxxxxx.x.xxxxxxxxxxxxxxxx.xx.xxxxxx.x.x.xxxxxxx.xxx.xt[SOLVER ERROR] {"python2 -u /home/sam/code/cuter/priv/cuter_interface.py --smt",
                [{{'__s',"0.1878130598.1640759297.34061"},
                  {2,
                   [{high,4},
                    {low,5},
                    {low,6},
                    {high,7},
                    {low,8},
                    {low,9},
                    {low,10},
                    {high,11}]}},
                 {{'__s',"0.1878130598.1640759297.34062"},
                  [{push,19},
                   {push,15},
                   {push,17},
                   {push,18},
                   {push,14},
                   {push,12},
                   {push,16},
                   pop,
                   {push,13},
                   add,pop]}],
                "/home/sam/code/cuter/stackmachine/temp/execexec13/run.trace",
                11}
Proccess <0.62.0> exited with {{solving,
                                   {unexpected_info,
                                       {'EXIT',#Port<0.1218>,normal}}},
                               {gen_fsm,sync_send_event,
                                   [<0.202.0>,check_model,500000]}}
Shutting down the execution...
Stopping poller <0.61.0>...
xx

No Runtime Errors Occured

sm.erl

-module(sm).
-export([multi_step/2
        ]).

-type lint() :: {low|high, integer()}.
-type instr() :: {push, integer()} | pop | add.
-type state() :: {non_neg_integer(), [lint()]}.
-type prog() :: [instr()].

-spec step(state(), prog()) -> state() | halt | {err, string()}.
step({PC, S}, Is) ->
  case nth(PC, Is) of
    none when PC =:= length(Is) -> halt;
    none -> {err, "pc out"};
    {push, _} -> {PC+1, [1|S]};
    pop ->
      case S of
        % err -> {err, "pop"};
        [_|S1] -> {PC+1, S1};
        _ -> {err, "pop"}
      end;
    add ->
      case S of
        [{_, X},{_,Y}|S2] -> {PC+1, [{low,X+Y}|S2]};
        _ -> {err, "add"}
      end
  end.

nth(0, [X|_]) -> X;
nth(N, [_|Xs]) -> nth(N-1, Xs);
nth(_, []) -> none.


-spec delete(pos_integer(), list()) -> list() | err.
delete(N, Xs) -> delete_(N, [], Xs).

delete_(0, Ys, [_|Xs]) -> Ys ++ Xs;
delete_(N, Ys, [X|Xs]) -> delete_(N-1, [X|Ys], Xs);
delete_(_, _, _) -> err.

-spec multi_step(state(), prog()) -> [integer()] | err.
multi_step(St = {_, S}, Is) ->
  case step(St, Is) of
    {err, _} -> err;
    halt -> S;
    St2 -> multi_step(St2, Is)
  end.