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

Remove redundant test

parent a6205d76
No related branches found
No related tags found
1 merge request!8Ajout du parsing de type de fonction polymorph.
Pipeline #30762 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 string 0)
(declare-fun index_bool (Bool) Int)
;; index_bool_True
(assert (= (index_bool true) 0))
;; index_bool_False
(assert (= (index_bool false) 1))
(declare-sort tuple0 0)
(declare-fun Tuple0 () tuple0)
(declare-fun x () Int)
(assert
;; Int_Pow1_invalid
;; File "test.mlw", line 7, characters 5-21
(not (<= x (colibri_pow_int_int 2 1025))))
(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