Commit 0ff35d55 authored by Mathias Preiner's avatar Mathias Preiner

Remove non-linear benchmarks.

parent 635fa5c5
(set-info :smt-lib-version 2.6)
(set-logic AUFBVDTLIA)
(set-info :source |
Generated by: Andrew Reynolds
Generated on: 2017-04-28
Generator: Nunchaku, Leon, CVC4, converted to v2.6 by CVC4
Application: Counterexample generation for higher-order theorem provers
Target solver: CVC4, Z3
Publications: "Model Finding for Recursive Functions in SMT" by Andrew Reynolds, Jasmin Christian Blanchette, Simon Cruanes, and Cesare Tinelli, IJCAR 2016.
|)
(set-info :license "https://creativecommons.org/licenses/by/4.0/")
(set-info :category "industrial")
(set-info :status unknown)
(declare-fun isPrime!205 (Int) Bool)
(declare-fun noneDivides!208 (Int Int) Bool)
(declare-fun divides!211 (Int Int) Bool)
(declare-sort I_isPrime!205 0)
(declare-fun isPrime!205_arg_0_1 (I_isPrime!205) Int)
(declare-sort I_noneDivides!208 0)
(declare-fun noneDivides!208_arg_0_2 (I_noneDivides!208) Int)
(declare-fun noneDivides!208_arg_1_3 (I_noneDivides!208) Int)
(declare-sort I_divides!211 0)
(declare-fun divides!211_arg_0_4 (I_divides!211) Int)
(declare-fun divides!211_arg_1_5 (I_divides!211) Int)
(assert (forall ((?i I_isPrime!205)) (and (= (isPrime!205 (isPrime!205_arg_0_1 ?i)) (and (noneDivides!208 2 (isPrime!205_arg_0_1 ?i)) (>= (isPrime!205_arg_0_1 ?i) 2))) (not (forall ((?z I_noneDivides!208)) (not (and (= (noneDivides!208_arg_0_2 ?z) 2) (= (noneDivides!208_arg_1_3 ?z) (isPrime!205_arg_0_1 ?i)))) ))) ))
(assert (forall ((?i I_noneDivides!208)) (and (= (noneDivides!208 (noneDivides!208_arg_0_2 ?i) (noneDivides!208_arg_1_3 ?i)) (ite (= (noneDivides!208_arg_0_2 ?i) (noneDivides!208_arg_1_3 ?i)) true (and (noneDivides!208 (+ 1 (noneDivides!208_arg_0_2 ?i)) (noneDivides!208_arg_1_3 ?i)) (not (divides!211 (noneDivides!208_arg_0_2 ?i) (noneDivides!208_arg_1_3 ?i)))))) (ite (= (noneDivides!208_arg_0_2 ?i) (noneDivides!208_arg_1_3 ?i)) true (and (not (forall ((?z I_noneDivides!208)) (not (and (= (noneDivides!208_arg_0_2 ?z) (+ 1 (noneDivides!208_arg_0_2 ?i))) (= (noneDivides!208_arg_1_3 ?z) (noneDivides!208_arg_1_3 ?i)))) )) (not (forall ((?z I_divides!211)) (not (and (= (divides!211_arg_0_4 ?z) (noneDivides!208_arg_0_2 ?i)) (= (divides!211_arg_1_5 ?z) (noneDivides!208_arg_1_3 ?i)))) ))))) ))
(assert (forall ((?i I_divides!211)) (= (divides!211 (divides!211_arg_0_4 ?i) (divides!211_arg_1_5 ?i)) (or (and (= (divides!211_arg_1_5 ?i) (* (divides!211_arg_0_4 ?i) (div (divides!211_arg_1_5 ?i) (divides!211_arg_0_4 ?i)))) (not (>= (+ (divides!211_arg_0_4 ?i) (* (- 1) (divides!211_arg_1_5 ?i))) 0))) (= (divides!211_arg_0_4 ?i) (divides!211_arg_1_5 ?i)))) ))
(assert (not (forall ((x!213 Int)) (>= x!213 201) )))
(check-sat)
(exit)
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment