1 files changed, 88 insertions, 0 deletions
diff --git a/tests/various/smtlib2_module-expected.smt2 b/tests/various/smtlib2_module-expected.smt2
new file mode 100644
index 000000000..bb869c08a
--- /dev/null
+++ b/tests/various/smtlib2_module-expected.smt2
@@ -0,0 +1,88 @@
+; SMT-LIBv2 description generated by Yosys $VERSION
+; yosys-smt2-module smtlib2
+(declare-sort |smtlib2_s| 0)
+(declare-fun |smtlib2_is| (|smtlib2_s|) Bool)
+(declare-fun |smtlib2#0| (|smtlib2_s|) (_ BitVec 8)) ; \a
+; yosys-smt2-input a 8
+(define-fun |smtlib2_n a| ((state |smtlib2_s|)) (_ BitVec 8) (|smtlib2#0| state))
+; yosys-smt2-output add 8
+(define-fun |smtlib2_n add| ((state |smtlib2_s|)) (_ BitVec 8) (let (
+(|a| (|smtlib2_n a| state))
+(|b| (|smtlib2_n b| state))
+)
+(bvadd a b)
+))
+(declare-fun |smtlib2#1| (|smtlib2_s|) (_ BitVec 8)) ; \b
+; yosys-smt2-input b 8
+(define-fun |smtlib2_n b| ((state |smtlib2_s|)) (_ BitVec 8) (|smtlib2#1| state))
+; yosys-smt2-output eq 1
+(define-fun |smtlib2_n eq| ((state |smtlib2_s|)) Bool (let (
+(|a| (|smtlib2_n a| state))
+(|b| (|smtlib2_n b| state))
+)
+(= a b)
+))
+; yosys-smt2-output sub 8
+(define-fun |smtlib2_n sub| ((state |smtlib2_s|)) (_ BitVec 8) (let (
+(|a| (|smtlib2_n a| state))
+(|b| (|smtlib2_n b| state))
+)
+(bvadd a (bvneg b))
+))
+(define-fun |smtlib2_a| ((state |smtlib2_s|)) Bool true)
+(define-fun |smtlib2_u| ((state |smtlib2_s|)) Bool true)
+(define-fun |smtlib2_i| ((state |smtlib2_s|)) Bool true)
+(define-fun |smtlib2_h| ((state |smtlib2_s|)) Bool true)
+(define-fun |smtlib2_t| ((state |smtlib2_s|) (next_state |smtlib2_s|)) Bool true) ; end of module smtlib2
+; yosys-smt2-module uut
+(declare-sort |uut_s| 0)
+(declare-fun |uut_is| (|uut_s|) Bool)
+; yosys-smt2-cell smtlib2 s
+(declare-fun |uut#0| (|uut_s|) (_ BitVec 8)) ; \add
+(declare-fun |uut#1| (|uut_s|) Bool) ; \eq
+(declare-fun |uut#2| (|uut_s|) (_ BitVec 8)) ; \sub
+(declare-fun |uut_h s| (|uut_s|) |smtlib2_s|)
+; yosys-smt2-anyconst uut#3 8 smtlib2_module.v:14.17-14.26
+(declare-fun |uut#3| (|uut_s|) (_ BitVec 8)) ; \a
+; yosys-smt2-anyconst uut#4 8 smtlib2_module.v:14.32-14.41
+(declare-fun |uut#4| (|uut_s|) (_ BitVec 8)) ; \b
+(define-fun |uut#5| ((state |uut_s|)) (_ BitVec 8) (bvadd (|uut#3| state) (|uut#4| state))) ; \add2
+(define-fun |uut#6| ((state |uut_s|)) Bool (= (|uut#0| state) (|uut#5| state))) ; $0$formal$smtlib2_module.v:28$1_CHECK[0:0]$9
+; yosys-smt2-assert 0 $assert$smtlib2_module.v:28$19 smtlib2_module.v:28.17-29.22
+(define-fun |uut_a 0| ((state |uut_s|)) Bool (or (|uut#6| state) (not true))) ; $assert$smtlib2_module.v:28$19
+(define-fun |uut#7| ((state |uut_s|)) (_ BitVec 8) (bvsub (|uut#3| state) (|uut#4| state))) ; \sub2
+(define-fun |uut#8| ((state |uut_s|)) Bool (= (|uut#2| state) (|uut#7| state))) ; $0$formal$smtlib2_module.v:29$2_CHECK[0:0]$11
+; yosys-smt2-assert 1 $assert$smtlib2_module.v:29$20 smtlib2_module.v:29.23-30.22
+(define-fun |uut_a 1| ((state |uut_s|)) Bool (or (|uut#8| state) (not true))) ; $assert$smtlib2_module.v:29$20
+(define-fun |uut#9| ((state |uut_s|)) Bool (= (|uut#3| state) (|uut#4| state))) ; $eq$smtlib2_module.v:31$17_Y
+(define-fun |uut#10| ((state |uut_s|)) Bool (= (ite (|uut#1| state) #b1 #b0) (ite (|uut#9| state) #b1 #b0))) ; $0$formal$smtlib2_module.v:30$3_CHECK[0:0]$13
+; yosys-smt2-assert 2 $assert$smtlib2_module.v:30$21 smtlib2_module.v:30.23-31.25
+(define-fun |uut_a 2| ((state |uut_s|)) Bool (or (|uut#10| state) (not true))) ; $assert$smtlib2_module.v:30$21
+(define-fun |uut_a| ((state |uut_s|)) Bool (and
+  (|uut_a 0| state)
+  (|uut_a 1| state)
+  (|uut_a 2| state)
+  (|smtlib2_a| (|uut_h s| state))
+))
+(define-fun |uut_u| ((state |uut_s|)) Bool 
+  (|smtlib2_u| (|uut_h s| state))
+)
+(define-fun |uut_i| ((state |uut_s|)) Bool 
+  (|smtlib2_i| (|uut_h s| state))
+)
+(define-fun |uut_h| ((state |uut_s|)) Bool (and
+  (= (|uut_is| state) (|smtlib2_is| (|uut_h s| state)))
+  (= (|uut#3| state) (|smtlib2_n a| (|uut_h s| state))) ; smtlib2.a
+  (= (|uut#0| state) (|smtlib2_n add| (|uut_h s| state))) ; smtlib2.add
+  (= (|uut#4| state) (|smtlib2_n b| (|uut_h s| state))) ; smtlib2.b
+  (= (|uut#1| state) (|smtlib2_n eq| (|uut_h s| state))) ; smtlib2.eq
+  (= (|uut#2| state) (|smtlib2_n sub| (|uut_h s| state))) ; smtlib2.sub
+  (|smtlib2_h| (|uut_h s| state))
+))
+(define-fun |uut_t| ((state |uut_s|) (next_state |uut_s|)) Bool (and
+  (= (|uut#4| state) (|uut#4| next_state)) ; $anyconst$5 \b
+  (= (|uut#3| state) (|uut#3| next_state)) ; $anyconst$4 \a
+  (|smtlib2_t| (|uut_h s| state) (|uut_h s| next_state))
+)) ; end of module uut
+; yosys-smt2-topmod uut
+; end of yosys output