aboutsummaryrefslogtreecommitdiffstats
path: root/verilog/Asm.v
diff options
context:
space:
mode:
Diffstat (limited to 'verilog/Asm.v')
-rw-r--r--verilog/Asm.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/verilog/Asm.v b/verilog/Asm.v
index 58e28c40..64ae1c32 100644
--- a/verilog/Asm.v
+++ b/verilog/Asm.v
@@ -1191,7 +1191,7 @@ Ltac Equalities :=
split. auto. intros. destruct B; auto. subst. auto.
- (* trace length *)
red; intros; inv H; simpl.
- omega.
+ lia.
eapply external_call_trace_length; eauto.
eapply external_call_trace_length; eauto.
- (* initial states *)