From ab8d44b83e210ed38623a1440e3ef1d318f7d0d0 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 21 Aug 2018 19:38:40 -0500 Subject: Fix processing of nested Variable construct in sygus let bodies (#2351) --- test/regress/regress1/sygus/let-bug-simp.sy | 22 ++++++++++++++++++++++ 1 file changed, 22 insertions(+) create mode 100644 test/regress/regress1/sygus/let-bug-simp.sy (limited to 'test/regress/regress1/sygus/let-bug-simp.sy') diff --git a/test/regress/regress1/sygus/let-bug-simp.sy b/test/regress/regress1/sygus/let-bug-simp.sy new file mode 100644 index 000000000..d570d5a21 --- /dev/null +++ b/test/regress/regress1/sygus/let-bug-simp.sy @@ -0,0 +1,22 @@ +; EXPECT: unsat +; COMMAND-LINE: --sygus-out=status +(set-logic LIA) + +(synth-fun f ((x0 Int) (x1 Int)) Bool +( + (StartInt Int (5)) + + (Start Bool ( + (let + ((z Int StartInt)) + (or + (= (Variable Int) z) + (= (Variable Int) z))))) +) +) + +(declare-var a Int) +(declare-var b Int) +(constraint (=> (= a 5) (f a b))) +(constraint (=> (= b 5) (f a b))) +(check-synth) -- cgit v1.2.3