diff --git a/deps/aig b/deps/aig index 00f138637d..adc0ca5666 160000 --- a/deps/aig +++ b/deps/aig @@ -1 +1 @@ -Subproject commit 00f138637d8936566534103878ca895613b7f714 +Subproject commit adc0ca56664804d5f1e7e8d8f794a5c1104068aa diff --git a/intTests/test1828/.gitignore b/intTests/test1828/.gitignore new file mode 100644 index 0000000000..2e31392fa5 --- /dev/null +++ b/intTests/test1828/.gitignore @@ -0,0 +1,2 @@ +left.aig +right.aig diff --git a/intTests/test1828/test.saw b/intTests/test1828/test.saw new file mode 100644 index 0000000000..f839820e50 --- /dev/null +++ b/intTests/test1828/test.saw @@ -0,0 +1,2 @@ +write_aig "left.aig" {{ \x -> x * 0x12345678 }}; +write_aig "right.aig" {{ \x -> 0x12345678 * x }}; diff --git a/intTests/test1828/test.sh b/intTests/test1828/test.sh new file mode 100755 index 0000000000..a914d55337 --- /dev/null +++ b/intTests/test1828/test.sh @@ -0,0 +1,9 @@ +set -e + +# This test case uses `write_aiger` to produce AIG files for two nearly +# identical functions, where the only difference is the order of arguments (one +# symbolic and one concrete) in a bitvector multiplication. If the `aig` library +# does its job correctly, these should produce identical AIG files, so check +# this using `diff`. +$SAW test.saw +diff -ru left.aig right.aig