blob: 959d83c7fbd60443ef78b93e9a7c74f153218d46 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
|
; EXPECT: unknown
; EXPECT: (:reason-unknown incomplete)
(set-logic AUFLIA)
(set-info :source |
Boogie/Spec# benchmarks.
This benchmark was translated by Michal Moskal.
|)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(set-info :status sat)
(declare-fun select2 (Int) Int)
(declare-fun store2 (Int) Int)
(assert (forall ((?A Int) (?o Int) (?f Int) (?p Int) (?g Int) (?v Int)) (=> (not (= ?o ?p)) (= (select2 (store2 ?A)) (select2 ?A)))))
(check-sat)
(get-info :reason-unknown)
(exit)
|
