gillian-js is unable to produce failing model for modifed Gillian-JS/Examples/Cosette/simple_example.js

[bjrjk]

I'm using the latest version of Gillian.
While the verification for original simple_example.js can be passed, after change the operator + to * according to https://gillianplatform.github.io/sphinx/js/symbolic-testing.html#assumptions-and-assertions , the verification cannot provide an counter example and crashes.
Changed simple_example.js is listed as follows:

var n1 = symb_number(), n2 = symb_number();

Assume((0 <= n1) and (0 <= n2) and (not (n1 = n2)));

var res = n1 * n2; // changed + to *

Assert((n1 <= res) and (n2 <= res));

var x = symb();
Assume(not (typeOf x = Obj));

var tx = typeof(x);

Original gillian-js output:

~/SymbolicExecution/Gillian$ dune exec -- gillian-js wpst Gillian-JS/Examples/Cosette/simple_example.js
Compilation time: 0.010296s              
Total time (Compilation + Symbolic testing): 5.172468s
Success!

Failed gillian-js output is attached with an .txt due to its tremendous text length.
failed_example.txt

[giltho]

Hi!
Well, the second assert shouldn't pass when using multiplication. Take n1 = 5 and n2 = 0.5, res is 2.5 and is less than n1. However, not quite sure why Gillian is failing to produce a simple model.
@NatKarmios could be your changes in the SMT connection, could you quickly investigate see what's happening and why we can't get a model?

[bjrjk]

Thanks a lot!

[klausnat]

Hello, yes, I am having very same problem... this is what I see instead of model

[giltho]

I'll investigate at some point, sorry for the lack of responsiveness, my PhD defence is next week 😬

[bjrjk]

No problem! As a PhD student, I understand your anxious feeling and that's totally understandable! The formal verification research is also very hard. Hope you will have a smooth defence and successfully graduate!