Project

General

Profile

Bug #5353

SAT regression benchs have very long runtime with --theoref

Added by Sepideh Asadi almost 2 years ago. Updated almost 2 years ago.

Status:
Feedback
Priority:
Normal
Start date:
24/06/2017
Due date:
% Done:

0%

Estimated time:

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 almost 2 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...

Also available in: Atom PDF