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

Add non regress case for bug22

parent 7391659b
No related branches found
No related tags found
1 merge request!10Fixes unsoundness2 #22
Pipeline #32651 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 integer 0)
(declare-sort t 0)
(declare-sort u 0)
(declare-sort v 0)
(declare-fun to_u (integer) u)
(declare-fun to_v (t u) v)
(declare-fun user_eq (v v) Bool)
(declare-const dummy v)
(declare-const x t)
(declare-const y t)
(declare-const z t)
(declare-const a integer)
(declare-const b integer)
(declare-const c integer)
(assert
;; defqtvc
;; File "member_alt.adb", line 1, characters 0-0
(not
(=
(not
(let ((tmp (to_v x (to_u a))))
(or (user_eq tmp (to_v y (to_u b)))
(user_eq tmp (to_v z (to_u c))))))
true)))
(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