Fix processing of nested Variable construct in sygus let bodies (#2351)

3 files changed, 85 insertions, 0 deletions

diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests
index e773bf698..f766396a1 100644
--- a/test/regress/Makefile.tests
+++ b/test/regress/Makefile.tests
@@ -1513,6 +1513,7 @@ REG1_TESTS = \
 	regress1/strings/type003.smt2 \
 	regress1/strings/username_checker_min.smt2 \
 	regress1/sygus/VC22_a.sy \
+	regress1/sygus/abv.sy \
 	regress1/sygus/array_search_2.sy \
 	regress1/sygus/array_search_5-Q-easy.sy \
 	regress1/sygus/array_sum_2_5.sy \
@@ -1546,6 +1547,7 @@ REG1_TESTS = \
 	regress1/sygus/inv-example.sy \
 	regress1/sygus/inv-unused.sy \
 	regress1/sygus/large-const-simp.sy \
+	regress1/sygus/let-bug-simp.sy \
 	regress1/sygus/list-head-x.sy \
 	regress1/sygus/logiccell_help.sy \
 	regress1/sygus/max.sy \
diff --git a/test/regress/regress1/sygus/abv.sy b/test/regress/regress1/sygus/abv.sy
new file mode 100644
index 000000000..6ce1a011a
--- /dev/null
+++ b/test/regress/regress1/sygus/abv.sy
@@ -0,0 +1,61 @@
+; EXPECT: unsat
+; COMMAND-LINE: --sygus-out=status
+(set-logic ABV)
+
+(define-sort AddrSort () (BitVec 32))
+(define-sort ValSort () (BitVec 8))
+(define-sort MemSort () (Array AddrSort ValSort))
+
+; Write the value y to index x
+(define-fun WriteArr 
+	; Args
+	((x AddrSort) (y ValSort) (arrIn MemSort)) 
+	
+	; Return value
+	MemSort
+	
+	; Function Body
+	(store arrIn x y)
+)
+
+; Read from index x
+(define-fun ReadArr 
+	; Args
+	((x AddrSort) (arrIn MemSort)) 
+	
+	; Return value
+	ValSort
+	
+	; Function Body
+	(select arrIn x)
+)
+
+
+(synth-fun f 
+	; Args
+	((x0 ValSort) (x1 ValSort) (idx0 AddrSort) (idx1 AddrSort) (mem MemSort))
+	
+	; Return value
+	ValSort
+    
+    	; Grammar
+    	(
+	(StartArray MemSort (
+		(WriteArr (Variable AddrSort) (Variable ValSort) StartArray)
+		(WriteArr (Variable AddrSort) (Variable ValSort) mem)))
+
+	(Start ValSort (
+		(let 
+			((m MemSort StartArray)) 
+			(bvadd 
+				(ReadArr (Variable AddrSort) m) 
+				(ReadArr (Variable AddrSort) m))))))
+)
+
+(declare-var a (BitVec 8))
+(declare-var b (BitVec 8))
+(declare-var c (BitVec 32))
+(declare-var d (BitVec 32))
+(declare-var e (Array (BitVec 32) (BitVec 8)))
+(constraint (=> (not (= c d)) (= (bvadd a b) (f a b c d e))))
+(check-synth)
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)