Sepideh Asadi comments

Results 9 comments of


                                            Sepideh Asadi

Printing CHCs after they have been simplified in Eldarica

Great, thanks!

Printing CHCs after they have been simplified in Eldarica

Thanks @pruemmer! Is there an option to print the simplified clauses in smt2 format, not prolog?

Printing CHCs after they have been simplified in Eldarica

Thanks @zafer-esen, I used the latest nightly build, very helpful! Would be great if this option appears in the official release as well.

Printing CHCs after they have been simplified in Eldarica

Thanks @zafer-esen and another followup feature request on this! It'd be great if the simplified clauses in SMT-LIB format are printed in a way that they are parsable & solvable...

Printing CHCs after they have been simplified in Eldarica

Cool! thank for the quick action on it @zafer-esen!

Printing CHCs after they have been simplified in Eldarica

Thanks for the update! I also have one question in the encoding: Here is the small java program: public class Main { public static int a; public static int b;...

Printing CHCs after they have been simplified in Eldarica

I am sharing all the original 5 SMT encodings generated by JayHorn, and also the simplified SMT encoding by Eldarica. [ex-asadi.zip](https://github.com/uuverifiers/eldarica/files/7346115/ex-asadi.zip)

Printing CHCs after they have been simplified in Eldarica

The stronger assert is reported safe by jayHorn as in the attachment. [stronger.zip](https://github.com/uuverifiers/eldarica/files/7354827/stronger.zip)

Printing CHCs after they have been simplified in Eldarica

Thanks @zafer-esen for checking that. Now I got the latest version and the encoding seems correct, thanks so much! After running your last command I get the following clauses after...