Skip to content
Snippets Groups Projects
Commit 83bb1b94 authored by François Bobot's avatar François Bobot
Browse files

Fixes #25

parent 2bb778bf
No related branches found
No related tags found
1 merge request!12Fix bug25
Pipeline #33671 passed
;; produced by colibri.drv ;;
(set-logic ALL)
(set-info :smt-lib-version 2.6)
;;; generated by SMT-LIB2 driver
;;; SMT-LIB2 driver: bit-vectors, common part
;;; SMT-LIB2: integer arithmetic
(declare-sort value 0)
(declare-fun valueqtint (value) Int)
(define-fun to_rep ((x value)) Int (valueqtint x))
(declare-const a (Array Int (Array Int value)))
(declare-const i Int)
(declare-const j Int)
(declare-const x value)
(declare-const y value)
(assert
(not
(= (to_rep
(select
(select
(store
(store a i
(store
(select a i)
j x))
i
(store
(select
(store a i
(store
(select a i)
j x))
i)
j y))
i)
j))
(to_rep
(select
(select
(store
(store a i
(store
(select a i)
j x))
i
(store
(select
(store a i
(store
(select a i)
j x))
i)
j y))
j)
i)))))
(check-sat)
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment