diff options
Diffstat (limited to 'test')
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress1/sygus/yoni-true-sol.smt2 | 20 |
2 files changed, 21 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 8aae1890d..06dc2d87c 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1951,6 +1951,7 @@ set(regress_1_tests regress1/sygus/unbdd_inv_gen_ex7.sy regress1/sygus/unbdd_inv_gen_winf1.sy regress1/sygus/univ_2-long-repeat.sy + regress1/sygus/yoni-true-sol.smt2 regress1/sym/q-constant.smt2 regress1/sym/q-function.smt2 regress1/sym/qf-function.smt2 diff --git a/test/regress/regress1/sygus/yoni-true-sol.smt2 b/test/regress/regress1/sygus/yoni-true-sol.smt2 new file mode 100644 index 000000000..464f7c729 --- /dev/null +++ b/test/regress/regress1/sygus/yoni-true-sol.smt2 @@ -0,0 +1,20 @@ +; COMMAND-LINE: --produce-abducts +; EXPECT: (define-fun A () Bool (>= j i)) +(set-logic QF_LIA) +(set-option :produce-abducts true) +(declare-fun n () Int) +(declare-fun m () Int) +(declare-fun i () Int) +(declare-fun j () Int) +(assert (and (>= n 0) (>= m 0))) +(assert (< n i)) +(assert (< (+ i j) m)) +(get-abduct A + (<= n m) + ((GA Bool) (GJ Int) (GI Int)) + ( + (GA Bool ((>= GJ GI))) + (GJ Int ( j)) + (GI Int ( i)) + ) +) |