diff --git a/tests/sat/issue_40_with_hyp.smt2 b/tests/sat/issue_40_with_hyp.smt2 new file mode 100644 index 0000000000000000000000000000000000000000..811fde090e1e7f748d075feb8b878a61c9682eac --- /dev/null +++ b/tests/sat/issue_40_with_hyp.smt2 @@ -0,0 +1,9 @@ +(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)