Fábio Pakk Selmi-Dei

icon indicating a website link https://www.linkedin.com/in/fabio-pakk-selmi-dei-08a5195/

icon company Cocotec icon location United Kingdom icon location Computer scientist specialized in the development of programming languages and tools such as compilers, static analyzers and formal verifiers. Expert in C++.

Results 5 comments of Fábio Pakk Selmi-Dei

Silicon hangs if smt code sent to Z3 isn't indented

Issue fixed. I've created a message for that now.

Silicon hangs if smt code sent to Z3 isn't indented

This solution slowed down Silicon, so I've removed the fix and reopened the issue.

Some unexpected output is occurring after merge of MagicWands

I addressed all warnings reported in this issue and pushed the changes into master branch.

"Packaging wand might fail" in Viper online example

Due to this bug, I've removed Carbon from the list of verifiers in Viper Online, for this example only. This removal should be reverted once this bug is fixed.

Failing arithmetic proofs (Z3)

This example is incomplete. @mschwerhoff could you please confirm the complete program is the following? ``` method m(a: Int, b: Int, n: Int, xs: Set[Int]){ inhale 0