Skip to content

Instantly share code, notes, and snippets.

@ahorn
ahorn / stp-performance-issue-101
Created May 4, 2014
Benchmark that causes the newest version of STP to timeout
View stp-performance-issue-101
(set-logic QF_BV)
(declare-fun v!0 () (_ BitVec 32))
(declare-fun v!1 () (_ BitVec 32))
(declare-fun v!2 () (_ BitVec 32))
(declare-fun v!3 () (_ BitVec 32))
(declare-fun v!4 () (_ BitVec 32))
(declare-fun v!5 () (_ BitVec 32))
(declare-fun v!6 () (_ BitVec 32))
(assert (and (and (and (and (and (and (and (and (and (and (and (not (bvsgt v!0 v!1)) (not (bvsgt v!0 v!2))) (not (bvsgt v!1 v!2))) (not (bvsgt v!0 v!3))) (bvsgt v!1 v!3)) (bvsgt v!0 v!4)) (bvsgt v!0 v!5)) (bvsgt v!4 v!5)) (bvsgt v!0 v!6)) (bvsgt v!4 v!6)) (not (bvsgt v!5 v!6))) (or (or (or (or (or (and (and (and (and (and (and (and (and (and (and (and (not (bvsgt v!0 v!1)) (not (bvsgt v!0 v!2))) (not (bvsgt v!1 v!2))) (not (bvsgt v!0 v!3))) (bvsgt v!1 v!3)) (bvsgt v!0 v!4)) (bvsgt v!0 v!5)) (bvsgt v!4 v!5)) (bvsgt v!0 v!6)) (bvsgt v!4 v!6)) (not (bvsgt v!5 v!6))) (bvsgt v!5 v!6)) (and (and (and (and (and (and (and (and (and (and (and (not (bvsgt v!0 v!1)) (not (bvsgt v!0 v!2))) (not (bvsgt v!1 v!2))) (not (bvsgt v!0 v!3))) (bvsgt v!1 v!3)) (bvsgt v!0