[BUG] LSP CN verify only works the first time it is run.

[kiranandcode]

Summary

I am running on MacOS Darwin, I have set up a local spam switch with the VERSE-toolchain as described on the readme. I am running the VScode LSP extension by opening the lsp-client folder in VScode and then pressing Cmd+Shift+B to build and run.

The newly opened VSCode instance works, and I can run CN on the current file, but this only works once.

Bug

If I try and run CN on the file again after making changes, after the first verification run which works correctly, every subsequent verification request fails. In the debug output panel on the lsp-client VSCode instance, I see the following exception being raised:

Verification failed with exception: ( "UnexpectedSolverResponse((error\
 \n \"line 56505 column 23: Invalid function declaration: unknown sort 'SLL_3542'\"))")

(I've made a modification to cn-lsp/lib/server.ml:run_cn which I've localised to be the location where this exception is thrown to catch it and print the above message.

The first verification run succeeds, so I believe this is something to do with some context being preserved across the subsequent runs causing the solver to fail.

[kiranandcode]

This is the full backtrace:

Raised at Cn__Solver.debug_ack_command in file "backend/cn/lib/solver.ml", line 164, characters 4-42
Called from Cn__Solver.ack_command in file "backend/cn/lib/solver.ml", line 197, characters 2-25
Called from Cn__Solver.translate_var in file "backend/cn/lib/solver.ml", line 683, characters 4-62
Called from Cn__Solver.translate_term in file "backend/cn/lib/solver.ml", line 891, characters 46-65
Called from Cn__Solver.translate_term in file "backend/cn/lib/solver.ml", line 751, characters 13-32
Called from Cn__Solver.translate_term in file "backend/cn/lib/solver.ml", line 732, characters 27-48
Called from Cn__Solver.model_evaluator.(fun).model_fn in file "backend/cn/lib/solver.ml", line 1374, characters 18-44
Called from Cn__Solver.eval in file "backend/cn/lib/solver.ml" (inlined), line 1437, characters 2-12
Called from Cn__Typing.model_has_prop.(fun) in file "backend/cn/lib/typing.ml", line 506, characters 37-70
Called from Cn__Typing.prove_or_model_with_past_model.res in file "backend/cn/lib/typing.ml", line 515, characters 18-44
Called from Cn__Typing.prove_or_model_with_past_model.res2 in file "backend/cn/lib/typing.ml", line 519, characters 22-28
Called from Cn__ResourcePredicates.identify_right_clause.try_clauses in file "backend/cn/lib/resourcePredicates.ml", line 91, characters 15-41
Called from Cn__Pack.packing_ft in file "backend/cn/lib/pack.ml", line 88, characters 14-70
Called from Cn__Pack.unpack in file "backend/cn/lib/pack.ml", line 139, characters 11-45
Called from Cn__Typing.do_unfold_resources.aux.(fun) in file "backend/cn/lib/typing.ml", line 705, characters 18-57
Called from Cn__Typing.do_unfold_resources.aux in file "backend/cn/lib/typing.ml", line 703, characters 8-859
Called from Cn__Typing.bind in file "backend/cn/lib/typing.ml", line 49, characters 17-20
Called from Cn__Typing.bind in file "backend/cn/lib/typing.ml", line 49, characters 17-20
Called from Cn__Typing.bind in file "backend/cn/lib/typing.ml", line 49, characters 17-20
Called from Cn__Typing.bind in file "backend/cn/lib/typing.ml", line 49, characters 17-20
Called from Cn__Typing.bind in file "backend/cn/lib/typing.ml", line 49, characters 17-20
Called from Cn__Typing.bind in file "backend/cn/lib/typing.ml", line 49, characters 17-20
Called from Cn__Typing.pure in file "backend/cn/lib/typing.ml", line 76, characters 22-25
Called from Cn__Typing.bind in file "backend/cn/lib/typing.ml", line 49, characters 17-20
Called from Cn__Typing.pure in file "backend/cn/lib/typing.ml", line 76, characters 22-25
Called from Cn__Typing.bind in file "backend/cn/lib/typing.ml", line 49, characters 17-20
Called from Cn__Typing.bind in file "backend/cn/lib/typing.ml", line 49, characters 17-20
Called from Cn__Typing.pure in file "backend/cn/lib/typing.ml", line 76, characters 22-25
Called from Cn__Typing.bind in file "backend/cn/lib/typing.ml", line 49, characters 17-20
Called from Cn__Typing.bind in file "backend/cn/lib/typing.ml", line 49, characters 17-20
Called from Cn__Typing.bind in file "backend/cn/lib/typing.ml", line 49, characters 17-20
Called from Cn__Typing.bind in file "backend/cn/lib/typing.ml", line 49, characters 17-20
Called from Cn__Typing.bind in file "backend/cn/lib/typing.ml", line 49, characters 17-20
Called from Cn__Typing.bind in file "backend/cn/lib/typing.ml", line 49, characters 17-20
Called from Cn__Typing.bind in file "backend/cn/lib/typing.ml", line 49, characters 17-20
Called from Cn__Typing.run in file "backend/cn/lib/typing.ml", line 60, characters 8-21
Called from Cnlsp__LspCn.CnM.let* in file "cn-lsp/lib/lspCn.ml" (inlined), line 130, characters 52-72
Called from Cnlsp__LspCn.run_cn in file "cn-lsp/lib/lspCn.ml", line 219, characters 8-450
Called from Cnlsp__Server.lsp_server#run_cn in file "cn-lsp/lib/server.ml", line 265, characters 23-39