Skip to content

Instantly share code, notes, and snippets.

ahorn

  • Oxford, UK
Block or report user

Report or block ahorn

Hide content and notifications from this user.

Learn more about blocking users

Contact Support about this user’s behavior.

Learn more about reporting abuse

Report abuse
View GitHub Profile
@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
You can’t perform that action at this time.