Bug #5353: SAT regression benchs have very long runtime with --theoref - hifrog - USI & SUPSI Source Code Management (SCM)

Actions

Bug #5353

open

SAT regression benchs have very long runtime with --theoref

Added by Sepideh Asadi over 7 years ago. Updated over 7 years ago.

Status:

Feedback

Priority:

Normal

Assignee:

Antti Hyvärinen

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.

Actions

#1

Updated by Karine Even Mendoza over 7 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...

Actions

Also available in: Atom PDF