Solver error

[Lysxia]

I'm trying out cuter to test abstract machine specifications, and I'm running into a solver error.
It's probably because I'm using protobuf/protoc-3.3.2 instead of 3.2 as mentioned in the README, but I'm hoping there is a simple fix.

I tried to minimize the example in this gist. A machine consists of a program counter, a stack (where values are labeled by some tag high | low) and a sequence of instructions: push a constant on the stack, pop the top of the stack, add the two elements at the top of the stack. I define a step function, and iterate it in multi_step. Running cuter on that function leads to the error.

./cuter -r -s 3 --depth 20 sm multi_step "[{0,[]},[]]"

OS/arch: ArchLinux 64bit
Versions:
- erlang 20.0.1
- python 2.7.14
- protobuf, protoc 3.3.1
- z3 4.5.0

[kostis]

OK, for what is worth, I can reproduce your error even with protoc-3.2.0, so this is not the culprit here. If the error was in Erlang code, I would investigate more, but since it's in the python communication, I will leave this for @aggelgian.

[kostis]

This does not solve the issue of course, but just in case it helps you achieving some progress in what you are doing, I discovered that if you take out |high (which is unused anyway in this code) from the type declaration of lint(), then there is no error -- for me at least.

[Lysxia]

Thanks! Unfortunately these tags are used in the semantics I'm actually interested in; I just tried to make as small an example of the error as I could, and indeed this tagging seems to be a trigger for that bug. Perhaps there is a workaround by implementing these tags with a different type, such as two lists instead of a list of pairs. I'll try again when I find the time.

[kostis]

@Lysxia Just in case it was not clear in my previous comment, the problem may be related to the fact that the high tag is not mentioned anywhere else in the program (code snippet).

[Lysxia]

Ah, I had misunderstood indeed!