Bug #5353
SAT regression benchs have very long runtime with --theoref
0%
Description
~/hi-bench/main-bench/theoref/bench_crafted/mod_mult_div1_bug.c is too slow.
div1_bug.c is too.
History
#1 Updated by Karine Even Mendoza over 6 years ago
- Status changed from New to Feedback
- Assignee changed from Sepideh Asadi to Antti Hyvärinen
- Priority changed from Low to Normal
I think here, all the code shall be refined. Can we get more steps in a step?
Also the solver seems to straggle a bit too long with the query...
It can also be a good candidate for theoref new heuristics and performance improvement.
Here is the query with --force: (if it can give a hint what we do need to improve/add)
(assert
(and
; XXX Partition: 0
(and (= (* |main::1::c!0#2| |main::1::b!0#2|) (* |main::1::b!0#2| |main::1::c!0#2|)) (and (= (* |main::1::c!0#2| |main::1::b!0#2|) (* |main::1::b!0#2| |main::1::c!0#2|)) (and (= (* |main::1::c!0#2| |main::1::b!0#2|) (* |main::1::b!0#2| |main::1::c!0#2|)) (and (= (* |main::1::c!0#2| |main::1::b!0#2|) (* |main::1::b!0#2| |main::1::c!0#2|)) (and (= (* |main::1::c!0#2| |main::1::b!0#2|) (* |main::1::b!0#2| |main::1::c!0#2|)) (and (= (* |main::1::c!0#2| |main::1::b!0#2|) (* |main::1::b!0#2| |main::1::c!0#2|)) (and (= |main::1::a!0#2| |symex::nondet#0|) (= |main::1::b!0#2| |symex::nondet#1|) (= |goto_symex::guard#1| (not (and (not (or (<= 10 |main::1::a!0#2|) (= |main::1::a!0#2| 10))) (or (<= 1 |main::1::a!0#2|) (= 1 |main::1::a!0#2|))))) (= |goto_symex::guard#2| (not (and (not (or (<= 10 |main::1::b!0#2|) (= |main::1::b!0#2| 10))) (or (<= 1 |main::1::b!0#2|) (= 1 |main::1::b!0#2|))))) (= |main::1::c!0#2| (/ |main::1::a!0#2| |main::1::b!0#2|)) (= (not (or (not |hifrog::fun_start#2|) (or (not (and (not |goto_symex::guard#1|) (not |goto_symex::guard#2|))) (= |main::1::a!0#2| (* |main::1::c!0#2| |main::1::b!0#2|))))) |hifrog::?err#1|) (or |hifrog::fun_start#2| (not |hifrog::fun_end#2|)))))))))
; XXX Partition: 1
(and (= (* |main::1::c!0#2| |main::1::b!0#2|) (* |main::1::b!0#2| |main::1::c!0#2|)) (and (= (* |main::1::c!0#2| |main::1::b!0#2|) (* |main::1::b!0#2| |main::1::c!0#2|)) (and (= (* |main::1::c!0#2| |main::1::b!0#2|) (* |main::1::b!0#2| |main::1::c!0#2|)) (and (= (* |main::1::c!0#2| |main::1::b!0#2|) (* |main::1::b!0#2| |main::1::c!0#2|)) (and (= (* |main::1::c!0#2| |main::1::b!0#2|) (* |main::1::b!0#2| |main::1::c!0#2|)) (and (= (* |main::1::c!0#2| |main::1::b!0#2|) (* |main::1::b!0#2| |main::1::c!0#2|)) (or |hifrog::fun_start#1| (not |hifrog::fun_end#1|))))))))
; XXX Partition: 2
(and (= (* |main::1::c!0#2| |main::1::b!0#2|) (* |main::1::b!0#2| |main::1::c!0#2|)) (and (= (* |main::1::c!0#2| |main::1::b!0#2|) (* |main::1::b!0#2| |main::1::c!0#2|)) (and (= (* |main::1::c!0#2| |main::1::b!0#2|) (* |main::1::b!0#2| |main::1::c!0#2|)) (and (= (* |main::1::c!0#2| |main::1::b!0#2|) (* |main::1::b!0#2| |main::1::c!0#2|)) (and (= (* |main::1::c!0#2| |main::1::b!0#2|) (* |main::1::b!0#2| |main::1::c!0#2|)) (and (= (* |main::1::c!0#2| |main::1::b!0#2|) (* |main::1::b!0#2| |main::1::c!0#2|)) (and |hifrog::?err#1| |hifrog::fun_start#1| (= |hifrog::fun_end#1| |hifrog::fun_start#2|) (= |return'!0#0| |symex::io::0|))))))))
))
(check-sat)
It looks lilke many * (mult), takes too much time...