From 870b29b0cce85941ed72d7e0ca75b61b0cfcf711 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Mon, 11 May 2015 11:53:07 +0200 Subject: [PATCH] Add missing regression. --- test/regress/regress0/sygus/const-var-test.sy | 26 +++++++++++++++++++ 1 file changed, 26 insertions(+) create mode 100644 test/regress/regress0/sygus/const-var-test.sy diff --git a/test/regress/regress0/sygus/const-var-test.sy b/test/regress/regress0/sygus/const-var-test.sy new file mode 100644 index 000000000..0d753bdf1 --- /dev/null +++ b/test/regress/regress0/sygus/const-var-test.sy @@ -0,0 +1,26 @@ +; EXPECT: unsat +; COMMAND-LINE: --cegqi-si + +(set-logic LIA) + +(synth-fun max2 ((x Int) (y Int)) Int + ((Start Int ((Variable Int) + (Constant Int) + (+ Start Start) + (- Start Start) + (ite StartBool Start Start))) + (StartBool Bool ((and StartBool StartBool) + (or StartBool StartBool) + (not StartBool) + (<= Start Start) + (= Start Start) + (>= Start Start))))) + +(declare-var x Int) +(declare-var y Int) + +(constraint (= (max2 x y) (+ x y 500))) + + +(check-synth) + -- 2.30.2