Tests issue #40 with hypothesis

ef0c5838 · François Bobot · e569c8c6 · ef0c5838
Commit ef0c5838 authored 3 years ago by François Bobot
--- a/tests/sat/issue_40_with_hyp.smt2
+++ b/tests/sat/issue_40_with_hyp.smt2
+(set-logic ALL)
+(set-info :smt-lib-version 2.6)
+(declare-const x Int)
+(declare-const y Int)
+(assert (not (= y 0)))
+(assert
+  (not (= (colibri_abs_int (colibri_cdiv x y))
+          (colibri_cdiv (colibri_abs_int x) (colibri_abs_int y)))))
+(check-sat)