(set-info :smt-lib-version 2.6)
(set-logic QF_UF)
(set-info :source |
Generated by: Aman Goel (amangoel@umich.edu), Karem A. Sakallah (karem@umich.edu)
Generated on: 2018-04-06

Generated by the tool Averroes 2 (successor of [1]) which implements safety property
verification on hardware systems.

This SMT problem belongs to a set of SMT problems generated by applying Averroes 2
to benchmarks derived from [2-5].

A total of 412 systems (345 from [2], 19 from [3], 26 from [4], 22 from [5]) were
syntactically converted from their original formats (using [6, 7]), and given to
Averroes 2 to perform property checking with abstraction (wide bit-vectors -> terms,
wide operators -> UF) using SMT solvers [8, 9].

[1] Lee S., Sakallah K.A. (2014) Unbounded Scalable Verification Based on Approximate
Property-Directed Reachability and Datapath Abstraction. In: Biere A., Bloem R. (eds)
Computer Aided Verification. CAV 2014. Lecture Notes in Computer Science, vol 8559.
Springer, Cham
[2] http://fmv.jku.at/aiger/index.html#beem
[3] http://www.cs.cmu.edu/~modelcheck/vcegar
[4] http://www.cprover.org/hardware/v2c
[5] http://github.com/aman-goel/verilogbench
[6] http://www.clifford.at/yosys
[7] http://github.com/chengyinwu/V3
[8] http://github.com/Z3Prover/z3
[9] http://github.com/SRI-CSL/yices2

id: paper_v3
query-maker: "Z3"
query-time: 1.145000 ms
query-class: abstract
query-category: assume
query-type: regular
status: unsat
|)
(set-info :license "https://creativecommons.org/licenses/by/4.0/")
(set-info :category "industrial")

;
(set-info :status unknown)
(declare-sort utt8 0)
(declare-fun z$n1s8 () utt8)
(declare-fun z$n255s8 () utt8)
(declare-fun z$n0s8 () utt8)
(declare-fun x () utt8)
(declare-fun y () utt8)
(declare-fun x$next () utt8)
(declare-fun y$next () utt8)
(declare-fun Gr_1_8_8 (utt8 utt8) Bool)
(declare-fun z$7 () Bool)
(declare-fun z$34 () Bool)
(declare-fun prop () Bool)
(declare-fun z$35 () Bool)
(declare-fun z$42 () Bool)
(declare-fun z$44 () Bool)
(declare-fun z$52 () Bool)
(declare-fun z$53 () Bool)
(declare-fun z$55 () Bool)
(declare-fun z$4 () Bool)
(declare-fun z$51 () Bool)
(declare-fun z$54 () Bool)
(declare-fun z$9 () Bool)
(declare-fun z$86 () Bool)
(declare-fun z$88 () Bool)
(declare-fun z$68 () Bool)
(declare-fun z$85 () Bool)
(declare-fun z$87 () Bool)
(declare-fun z$120 () Bool)
(declare-fun p$0 () Bool)
(assert
 (and (distinct z$n0s8 z$n255s8 z$n1s8) true))
(assert
 (let (($x243 (Gr_1_8_8 y x)))
 (= z$7 $x243)))
(assert
 (let (($x91 (not z$7)))
 (= z$34 $x91)))
(assert
 (= z$35 (= prop z$34)))
(assert
 (= z$42 (not prop)))
(assert
 (let (($x73 (Gr_1_8_8 y$next x$next)))
 (= z$44 $x73)))
(assert
 (let (($x157 (= y$next z$n0s8)))
 (= z$52 $x157)))
(assert
 (= z$53 (and z$44 z$52)))
(assert
 (= z$55 (not z$53)))
(assert
 (let (($x78 (= y z$n0s8)))
 (= z$4 $x78)))
(assert
 (= z$51 (and z$7 z$4)))
(assert
 (= z$54 (not z$51)))
(assert
 (let (($x252 (= y x)))
 (= z$9 $x252)))
(assert
 (= z$86 (and z$9 z$7)))
(assert
 (= z$88 (not z$86)))
(assert
 (let (($x284 (= x$next y$next)))
 (= z$68 $x284)))
(assert
 (= z$85 (and z$68 z$44)))
(assert
 (= z$87 (not z$85)))
(assert
 (= z$120 (and z$35 z$42 z$55 z$54 z$88 z$87)))
(assert
 z$120)
(assert
 (let (($x252 (= y x)))
 (let (($x89 (= z$9 $x252)))
 (=> p$0 $x89))))
(assert
 (=> p$0 z$9))
(check-sat)
(assert p$0)
(check-sat)
(exit)