Reach Compiler Error

[BunsanMuchi]

Hi, I got the following error when trying to turn on verifyPerConnector

Compiling "main"...
Verifying knowledge assertions
Verifying for ALGO connector
  Verifying when ALL participants are honest
reachc: The compiler has encountered an internal error:

  Unexpected result from the SMT solver:
  Expected: success
  Result: (error "line 118 column 32: unknown constant T0_cons (Int Int Int ) declared: (declare-fun T0_cons (Token Token Token ) (Array Int Token ) ) " )


This error indicates a problem with the Reach compiler, not your program. Please report this error, along with the pertinent program, to the Reach team as soon as possible so we can fix it.

Open an issue at: https://github.com/reach-sh/reach-lang/issues

CallStack (from HasCallStack):
  error, called at src/Reach/Util.hs:65:3 in reach-0-ILn78w7tAsfKMai7G6d7pp:Reach.Util
  impossible, called at src/Reach/Verify/SMT.hs:724:9 in reach-0-ILn78w7tAsfKMai7G6d7pp:Reach.Verify.SMT

If I delete the flag the error goes away.

[jeapostrophe]

Thank you! Can you privately send me the code? (Also, I assume you're on the latest release of Reach?)

[jeapostrophe]

Closed for no report