Add test

intTests/test_join_split/README.md

@@ -0,0 +1,7 @@
+This test addresses the issue resolved in [#1790](https://github.com/GaloisInc/saw-script/pull/1790). 
+
+In this script, we prove the same theorem - that ```join`{each=32, parts=4, a=Bool} (split x) == x``` - twice; once purely via `z3`, and once via manual rewriting, trying to use the former to prove the latter. 
+
+Lack of type normalization introduces reflexive type coercions in the SAWCore representation of the expression under proof. The manual proof proceeds by eliminating any extant reflexive coercions, then attempting to use the `z3`-proven theorem as a simplification. When no coercions existed in the first place, the simplification applies cleanly. When coercions existed, the simplification does not apply cleanly, since we eliminated them from the goal, but not from the simplification.
+
+Since this proof is possible to resolve in its entirety via evaluation/appeal to `z3`, we need to maintain the core `join` and `split` functions uninterpreted when manually massaging (via `goal_normalize` and `goal_eval_unint`) the goal into a `trivial`ly resolvable form.

intTests/test_join_split/join_split.saw

@@ -0,0 +1,10 @@
+enable_experimental; // for `goal_normalize`
+
+join_split_thm_z3 <- prove_print z3 {{ \x -> join`{each=32, parts=4, a=Bool} (split x) == x }};
+
+join_split_thm_manual <- prove_print (do {
+    goal_normalize ["ecJoin", "ecSplit"];
+    simplify (addsimp join_split_thm_z3 empty_ss);
+    goal_eval_unint ["ecJoin", "ecSplit"];
+    trivial;
+}) {{ \x -> join`{each=32, parts=4, a=Bool} (split x) == x }};

intTests/test_join_split/test.sh

@@ -0,0 +1,3 @@
+#!/usr/bin/env bash
+
+$SAW join_split.saw