search

kperun / SATPrakPDW

Interval Constraint Propagation strategy implementation for SMTRAT
MIT License
2 stars 0 forks source link

Segfaults #51

Closed kperun closed 7 years ago

kperun commented 7 years ago

The benchmark shows that, in some cases, segfaults and memouts occure. The following problems contained segfaults: /hycomp/ball_count_2d_hill.01.redlog_global_15.smt2 /hycomp/ball_count_2d_hill.03.redlog_global_14.smt2 hycomp/ball_count_2d_hill.03.redlog_global_15.smt2 /hycomp/ball_count_2d_hill.05.redlog_global_14.smt2 /hycomp/ball_count_2d_hill.05.redlog_global_15.smt2 /hycomp/ball_count_2d_hill.10.redlog_global_14.smt2 hycomp/etcs_braking_2.01.redlog_global_14.smt2 hycomp/etcs_braking_2.01.redlog_global_15.smt2 hycomp/simple_ballistics_reach.01.seq_lazy_lemmas_global_14.smt2 meti-tarski/Arthan/1A/Arthan1A-chunk-0021.smt2 meti-tarski/atan/problem/2/atan-problem-2-chunk-0011.smt2 meti-tarski/atan/problem/2/atan-problem-2-chunk-0012.smt2 meti-tarski/atan/problem/2/atan-problem-2-chunk-0109.smt2 meti-tarski/atan/problem/2/weak/atan-problem-2-weak-chunk-0009.smt2 meti-tarski/atan/problem/2/weak/atan-problem-2-weak-chunk-0010.smt2 meti-tarski/polypaver/sqrt-circles/2a/polypaver-sqrt-circles-2a-chunk-0015.smt2

kperun commented 7 years ago

After some sample tests, it seems that the segfaults do not occur in every execution. On my machine, the execution of e.g. atan-problem-2-weak-chunk-0010 did not contain any errors or segfaults. @DavidWz and @Verdict7 would you mind testing the stated problems?

DavidWz commented 7 years ago

I tested the meti-tarski problems and got SAT in all cases. Never segfaults. However, I couldn't find the hycomp examples. I think they are using a different set of benchmark examples? The files also don't have "bounded" in their names, so are they using unbounded versions? We have to ask them.

kperun commented 7 years ago

Moreover, the timeframe in which a problem has to be solved is limited (if I recall correctly it was 30 seconds), as well as the amount of memory (4 gigs). However, I think this is something that we can not actively test. We should desist from using an artificial limitation of the maximal computation time, but use, as @DavidWz already mentioned, an indirect limitation, e.g. by setting the number of splits etc.

DavidWz commented 7 years ago

I looked at the segfaults in the latest benchmark, and again, I cannot reproduce any of them. I always get sat or unsat. @kperun Do you have an example problem which leads to a segfault?

DavidWz commented 7 years ago

Okay, the segfaults happened not in the bounded.zip examples but in their QF_NRA examples. I could reproduce them and fixed a lot of them in commit 0ac5bcf.