hifrog

h1. Skype Meeting 06092016

*Generally discussed in the meeting*

- Benchmarks

- Testing of last changes in opensmt

- Refinement

- UF encoding

- Cprover upgrade

*Updates of current tasks:*

Antti: works on incrementality- added some bugs to Issue-tracking

Karine: is working on new version of CBMC- and refinement.

Sepideh: is doing experiments on FF-HF-CBMC

sepideh has found some benchmarks that CBMC gets out of memory, but HiFrog and Funfrog managed to do verification very quickly.

Benchmarks: EvenOdd.c, Arith.c, in recursion directory

reports some bugs: rec4.c  in 17_recursion which HIfrog failed with this error:; Error: Clause has no color (triggered at PGInterAux.C, 218)

=========================================

*Things we agreed to do this week:*

Antti: Uploaded the benchmark of Milano guys, FABRIZIO PASTORE,(also will upload more)

Karine:

1. Upload some of SIR benchmarks

2. Refinement - checking + reporting bugs

3. Continue update cprover/cbmc 5.5

4. Generally check hifrog with LRA after the last changes in opensmt

   ==> There are some bugs, I added comments and will open a new ticket if needed

5. Test refinement - #3488 issue number, several problems

   ==> Added a comment with the smt encoding we are sending to the solver

6. To check if it is the same ptref - check the field - PTRef::x

   ==> Added it to the prints + some testing. Need to test it with the original benchmark that causes the bug

7. Check the reason for improvement

7.1 funfrog - hifrog check

7.2 opensmt - opensmt2 check

8. Open new branch EUF in two weeks + start working on UF encoding (Theory.h in opensmt).

Sepideh:

1) We need to know how consistent the results of experiment are, so Sepideh will prepare Scatter plot, and compare the results.

2) she will do experiment on Milano guys' benchmark.

3) Doing new experiments: compare total time for some benchmarks in both incremental and non-incremental on propositional OpenSMT2 

--------------

We need to have proper benchmark for interpolation.