Skip to content

Commit 1570909

Browse files
committed
fixes #414
1 parent 8e7f8fa commit 1570909

File tree

1 file changed

+19
-2
lines changed

1 file changed

+19
-2
lines changed

src/terms/term_manager.c

Lines changed: 19 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -3998,11 +3998,28 @@ term_t mk_constant(term_manager_t *manager, type_t tau, int32_t i) {
39983998
* - i.e., this creates a fresh global variable
39993999
*/
40004000
term_t mk_uterm(term_manager_t *manager, type_t tau) {
4001+
term_table_t *table;
4002+
int_hmap_pair_t *p;
4003+
term_t t;
4004+
4005+
table = manager->terms;
4006+
4007+
// Create a new uninterpreted term
40014008
if (is_unit_type(manager->types, tau)) {
4002-
return get_unit_type_rep(manager->terms, tau);
4009+
// Check if we already have an uninterpreted term for unit type
4010+
p = int_hmap_find(&table->utbl, tau);
4011+
if (p != NULL) {
4012+
return p->val;
4013+
} else {
4014+
t = new_uninterpreted_term(table, tau);
4015+
// Store it in the table
4016+
p = int_hmap_get(&table->utbl, tau);
4017+
p->val = t;
4018+
return t;
4019+
}
40034020
}
40044021

4005-
return new_uninterpreted_term(manager->terms, tau);
4022+
return new_uninterpreted_term(table, tau);
40064023
}
40074024

40084025

0 commit comments

Comments
 (0)