Memory and value refinement should be checked together if there's nondet exec.
ADD
tests/alive-tv/refinement/nondet-fail.srctgt.ll
+define i1 @src() {
+ %guard = freeze i1 undef
+ br i1 %guard, label %COMPARE, label %EXIT
+
+COMPARE:
+ call void @g()
+ ret i1 1
+
+EXIT:
+ ret i1 0
+}
+
+define i1 @tgt() {
+ %guard = freeze i1 undef
+ br i1 %guard, label %COMPARE, label %EXIT
+
+COMPARE:
+ ret i1 1
+
+EXIT:
+ ret i1 0
+}
+
+declare void @g()
+
+; ERROR: Mismatch in memory

ADD
tests/alive-tv/refinement/nondet-fail2.srctgt.ll
+define i1 @src() {
+ %guard = freeze i1 undef
+ br i1 %guard, label %COMPARE, label %EXIT
+
+COMPARE:
+ call void @g()
+ ret i1 1
+
+EXIT:
+ ret i1 0
+}
+
+define i1 @tgt() {
+ %guard = freeze i1 undef
+ br i1 %guard, label %COMPARE, label %EXIT
+
+COMPARE:
+ call void @g()
+ ret i1 0
+
+EXIT:
+ ret i1 1
+}
+
+declare void @g()
+
+; ERROR: Mismatch in memory

MODIFY
tools/transform.cpp
tools/transform.cpp
@@ -328,8 +328,9 @@ check_refinement(Errors &errs, Transform &t, State &src_state, State &tgt_state,
auto src_mem = src_state.returnMemory();
auto tgt_mem = tgt_state.returnMemory();
- auto [memory_cnstr, ptr_refinement0] = src_mem.refined(tgt_mem, false);
+ auto [memory_cnstr0, ptr_refinement0] = src_mem.refined(tgt_mem, false);
auto &ptr_refinement = ptr_refinement0;
+ auto memory_cnstr = value_cnstr && memory_cnstr0;
if (check_expr(axioms_expr && (pre_src && pre_tgt)).isUnsat()) {
errs.add("Precondition is always false", false);

Memory and value refinement should be checked together if there's nondet exec. (#392)