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

Fix some tests

parent e1bcb3df
No related branches found
No related tags found
1 merge request!8Ajout du parsing de type de fonction polymorph.
;; produced by colibri.drv ;; ;; produced by colibri.drv ;;
(set-logic QF_NIRABVFP) (set-logic ALL)
(set-info :smt-lib-version 2.6) (set-info :smt-lib-version 2.6)
;;; generated by SMT-LIB2 driver ;;; generated by SMT-LIB2 driver
;;; SMT-LIB2 driver: bit-vectors, common part ;;; SMT-LIB2 driver: bit-vectors, common part
......
;; produced by colibri.drv ;; ;; produced by colibri.drv ;;
(set-logic QF_NIRABVFP) (set-logic ALL)
(set-info :smt-lib-version 2.6) (set-info :smt-lib-version 2.6)
;;; generated by SMT-LIB2 driver ;;; generated by SMT-LIB2 driver
;;; SMT-LIB2 driver: bit-vectors, common part ;;; SMT-LIB2 driver: bit-vectors, common part
......
;; produced by colibri.drv ;; ;; produced by colibri.drv ;;
(set-logic QF_NIRABVFP) (set-logic ALL)
(set-info :smt-lib-version 2.6) (set-info :smt-lib-version 2.6)
;;; generated by SMT-LIB2 driver ;;; generated by SMT-LIB2 driver
;;; SMT-LIB2 driver: bit-vectors, common part ;;; SMT-LIB2 driver: bit-vectors, common part
......
(set-info :smt-lib-version 2.6) (set-info :smt-lib-version 2.6)
;;; Processed by pysmt to remove constant-real bitvector literals ;;; Processed by pysmt to remove constant-real bitvector literals
(set-logic QF_FP) (set-logic QF_UFFP)
(set-info :source |SPARK inspired floating point problems by Florian Schanda|) (set-info :source |SPARK inspired floating point problems by Florian Schanda|)
(set-info :category "crafted") (set-info :category "crafted")
(set-info :status unsat) (set-info :status unsat)
......
(set-info :smt-lib-version 2.6) (set-info :smt-lib-version 2.6)
;;; Processed by pysmt to remove constant-real bitvector literals ;;; Processed by pysmt to remove constant-real bitvector literals
(set-logic QF_FP) (set-logic QF_UFFP)
(set-info :source |SPARK inspired floating point problems by Florian Schanda|) (set-info :source |SPARK inspired floating point problems by Florian Schanda|)
(set-info :category "crafted") (set-info :category "crafted")
(set-info :status unsat) (set-info :status unsat)
......
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